Cross Reference: /hets/Isabelle/export/parser.ml

Lines Matching refs:option
2 	type opt_target = (xstring * Position.T) option;
43         |Definition of opt_target * ((binding * string option * mixfix) option
46                           ((binding * string option * mixfix) option * string))
52         |Axiomatization of (binding * string option * mixfix) list *
56                      (binding * string option * mixfix) list
59                      (binding * string option * mixfix) list
61                     (binding * string option * mixfix) list
83                     (binding * string option * mixfix) list
101 	|Instance of (instance_type option) * proof
123         |Primrec of (opt_target * (binding * string option * mixfix) list) *
128                  string option * mixfix) list) *
130         |PartialFunction of xstring * ((binding * string option * mixfix) list *
133                        (binding * string option * mixfix) list)
135         |Termination of string option * proof
136         |Typedef of (((((string * string option) list * binding) * mixfix) *
137           string) * (binding * binding) option) * proof
138         |Fixrec of opt_target * ((binding * string option * mixfix) list *
140 	|Domain of bool * ((((string * string option) list * binding) * mixfix)             * ((binding * (bool * binding option * string) list) * mixfix) list)
327                          (opt_mode -- (Scan.option
434 	("instance",Scan.option (                          (* line 481 *)
472         ("termination",Scan.option Parse.term -- proof
478          Scan.option (@{keyword "morphisms"} |--
493                   in Parse.enum1 "|" (spec' --| Scan.option
499           let val dest_decl : (bool * binding option * string) parser =
640 	datatype thy = Thy of {header:string option,
645 	val read_sort : Toplevel.state -> (string * Position.T) option
647 	val read_typ  : Toplevel.state -> (string * Position.T) option
650                          (string * Position.T) option -> string -> term
651         val read_prop : Toplevel.state -> (string * Position.T) option ->
653 	val read_class : Toplevel.state -> (string * Position.T) option ->
656                              (string * Position.T) option -> typ
668                                   typ option -> mixfix
674         datatype thy = Thy of {header:string option,
688 	val thy = Scan.catch (Scan.option cmd_header -- cmd_theory