--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Thu Mar 15 20:07:00 2012 +0100
@@ -229,21 +229,21 @@
(** outer syntax **)
val dest_decl : (bool * binding option * string) parser =
- Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
- (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1
- || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
- >> (fn t => (true,NONE,t))
- || Parse.typ >> (fn t => (false,NONE,t))
+ @{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false --
+ (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ) --| @{keyword ")"} >> Parse.triple1
+ || @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"}
+ >> (fn t => (true, NONE, t))
+ || Parse.typ >> (fn t => (false, NONE, t))
val cons_decl =
Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix
val domain_decl =
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
- (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl)
+ (@{keyword "="} |-- Parse.enum1 "|" cons_decl)
val domains_decl =
- Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
+ Scan.optional (@{keyword "("} |-- (@{keyword "unsafe"} >> K true) --| @{keyword ")"}) false --
Parse.and_list1 domain_decl
fun mk_domain
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Mar 15 20:07:00 2012 +0100
@@ -762,8 +762,8 @@
val parse_domain_iso :
(string list * binding * mixfix * string * (binding * binding) option)
parser =
- (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
+ (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs))
val parse_domain_isos = Parse.and_list1 parse_domain_iso
--- a/src/HOL/HOLCF/Tools/cpodef.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Thu Mar 15 20:07:00 2012 +0100
@@ -344,13 +344,13 @@
(** outer syntax **)
val typedef_proof_decl =
- Scan.optional (Parse.$$$ "(" |--
- ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Scan.optional (@{keyword "("} |--
+ ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
Parse.binding >> (fn s => (true, SOME s)))
- --| Parse.$$$ ")") (true, NONE) --
+ --| @{keyword ")"}) (true, NONE) --
(Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
- (Parse.$$$ "=" |-- Parse.term) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
+ (@{keyword "="} |-- Parse.term) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
--- a/src/HOL/HOLCF/Tools/domaindef.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Thu Mar 15 20:07:00 2012 +0100
@@ -212,13 +212,13 @@
(** outer syntax **)
val domaindef_decl =
- Scan.optional (Parse.$$$ "(" |--
- ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Scan.optional (@{keyword "("} |--
+ ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
Parse.binding >> (fn s => (true, SOME s)))
- --| Parse.$$$ ")") (true, NONE) --
+ --| @{keyword ")"}) (true, NONE) --
(Parse.type_args_constrained -- Parse.binding) --
- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
--- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Mar 15 20:07:00 2012 +0100
@@ -391,15 +391,15 @@
(*************************************************************************)
val opt_thm_name' : (bool * Attrib.binding) parser =
- Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
+ @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding)
|| Parse_Spec.opt_thm_name ":" >> pair false
val spec' : (bool * (Attrib.binding * string)) parser =
opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)))
val alt_specs' : (bool * (Attrib.binding * string)) list parser =
- let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(")
- in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end
+ let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
+ in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
val _ =
Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Mar 15 20:07:00 2012 +0100
@@ -673,14 +673,14 @@
Outer_Syntax.local_theory_to_proof "nominal_inductive"
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
Keyword.thy_goal
- (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
- (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
+ (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
+ (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
Outer_Syntax.local_theory "equivariance"
"prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
- (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
+ (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
end
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Mar 15 20:07:00 2012 +0100
@@ -488,9 +488,9 @@
"prove strong induction theorem for inductive predicate involving nominal datatypes"
Keyword.thy_goal
(Parse.xname --
- Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
- (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
- (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
+ Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
+ (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
+ (@{keyword ":"} |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
prove_strong_ind name rule_name avoids));
end
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Mar 15 20:07:00 2012 +0100
@@ -392,14 +392,14 @@
val freshness_context = Parse.reserved "freshness_context";
val invariant = Parse.reserved "invariant";
-fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- @{keyword ":"}) scan;
-val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
-val parser2 = (invariant -- Parse.$$$ ":") |--
+val parser1 = (freshness_context -- @{keyword ":"}) |-- unless_flag Parse.term >> SOME;
+val parser2 = (invariant -- @{keyword ":"}) |--
(Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
(parser1 >> pair NONE);
val options =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
+ Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
val _ =
Outer_Syntax.local_theory_to_proof "nominal_primrec"
--- a/src/HOL/Statespace/state_space.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Statespace/state_space.ML Thu Mar 15 20:07:00 2012 +0100
@@ -676,15 +676,15 @@
val type_insts =
Parse.typ >> single ||
- Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
+ @{keyword "("} |-- Parse.!!! (Parse.list1 Parse.typ --| @{keyword ")"})
-val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
+val comp = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.typ);
fun plus1_unless test scan =
- scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
+ scan ::: Scan.repeat (@{keyword "+"} |-- Scan.unless test (Parse.!!! scan));
-val mapsto = Parse.$$$ "=";
+val mapsto = @{keyword "="};
val rename = Parse.name -- (mapsto |-- Parse.name);
-val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
+val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
val parent =
((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
@@ -694,10 +694,10 @@
val statespace_decl =
Parse.type_args -- Parse.name --
- (Parse.$$$ "=" |--
+ (@{keyword "="} |--
((Scan.repeat1 comp >> pair []) ||
(plus1_unless comp parent --
- Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])));
+ Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
val _ =
Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
(statespace_decl >> (fn ((args, name), (parents, comps)) =>
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Mar 15 20:07:00 2012 +0100
@@ -788,7 +788,7 @@
val spec_cmd =
Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
- (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
+ (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =
--- a/src/HOL/Tools/Function/function_common.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Thu Mar 15 20:07:00 2012 +0100
@@ -345,7 +345,7 @@
|| (Parse.reserved "no_partials" >> K No_Partials))
fun config_parser default =
- (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
+ (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
--- a/src/HOL/Tools/Function/partial_function.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Thu Mar 15 20:07:00 2012 +0100
@@ -279,7 +279,7 @@
val add_partial_function = gen_add_partial_function Specification.check_spec;
val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
-val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
+val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
val _ = Outer_Syntax.local_theory
"partial_function" "define partial function" Keyword.thy_decl
--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Mar 15 20:07:00 2012 +0100
@@ -292,7 +292,7 @@
val parse_metis_options =
Scan.optional
(Args.parens (Parse.short_ident
- -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
+ -- Scan.option (@{keyword ","} |-- Parse.short_ident))
>> (fn (s, s') =>
(NONE, NONE) |> consider_opt s
|> (case s' of SOME s' => consider_opt s' | _ => I)))
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 15 20:07:00 2012 +0100
@@ -317,11 +317,11 @@
Scan.repeat1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus
(Parse.name || Parse.float_number))
- || Parse.$$$ "," |-- Parse.number >> prefix "," >> single)
+ || @{keyword ","} |-- Parse.number >> prefix "," >> single)
>> flat
-val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
val parse_params =
- Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
+ Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
fun handle_exceptions ctxt f x =
f x
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Mar 15 20:07:00 2012 +0100
@@ -1002,7 +1002,7 @@
(* renewing the values command for Prolog queries *)
val opt_print_modes =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Mar 15 20:07:00 2012 +0100
@@ -221,15 +221,15 @@
val opt_modes =
- Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
- (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
+ Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |--
+ (((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} --
(Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
|| ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
- --| Parse.$$$ ")") (Multiple_Preds [])
+ --| @{keyword ")"}) (Multiple_Preds [])
val opt_expected_modes =
- Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
- Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
+ Scan.optional (@{keyword "("} |-- Args.$$$ "expected_modes" |-- @{keyword ":"} |--
+ Parse.enum "," parse_mode_expr --| @{keyword ")"} >> SOME) NONE
(* Parser for options *)
@@ -238,18 +238,18 @@
val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
in
- Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
- -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
+ Scan.optional (@{keyword "["} |-- Scan.optional scan_compilation Pred
+ -- Parse.enum "," scan_bool_option --| @{keyword "]"})
(Pred, [])
end
val opt_print_modes =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
-val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
+val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
-val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
- Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
+val opt_param_modes = Scan.optional (@{keyword "["} |-- Args.$$$ "mode" |-- @{keyword ":"} |--
+ Parse.enum ", " opt_mode --| @{keyword "]"} >> SOME) NONE
val stats = Scan.optional (Args.$$$ "stats" >> K true) false
@@ -264,7 +264,7 @@
(Pred, [])
in
Scan.optional
- (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
+ (@{keyword "["} |-- (expected_values -- stats) -- scan_compilation --| @{keyword "]"})
((NONE, false), (Pred, []))
end
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 15 20:07:00 2012 +0100
@@ -66,8 +66,8 @@
val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
Keyword.thy_decl ((Parse.type_const --
- Scan.option (Args.$$$ "predicate" |-- Parse.$$$ ":" |-- Parse.term)) --
- (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
+ Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
+ (Args.$$$ "constructors" |-- @{keyword ":"} |-- Parse.list1 Parse.term)
>> (fn ((tyco, opt_pred), constrs) =>
Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Mar 15 20:07:00 2012 +0100
@@ -109,7 +109,7 @@
(* parser and command *)
val quotdef_parser =
Scan.option Parse_Spec.constdecl --
- Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
+ Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
val _ =
Outer_Syntax.local_theory "quotient_definition"
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 15 20:07:00 2012 +0100
@@ -71,7 +71,7 @@
val quotmaps_attribute_setup =
Attrib.setup @{binding map}
- ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) -- (* FIXME Args.type_name true (requires "set" type) *)
+ ((Args.type_name false --| Scan.lift (@{keyword "="})) -- (* FIXME Args.type_name true (requires "set" type) *)
Args.const_proper true >>
(fn (tyname, relname) =>
let val minfo = {relmap = relname}
--- a/src/HOL/Tools/Quotient/quotient_type.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Thu Mar 15 20:07:00 2012 +0100
@@ -262,15 +262,15 @@
quotient_type spec' lthy
end
-val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
+val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
val quotspec_parser =
Parse.and_list1
((Parse.type_args -- Parse.binding) --
(* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
- (Parse.$$$ "/" |-- (partial -- Parse.term)) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+ (@{keyword "/"} |-- (partial -- Parse.term)) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
val _ =
Outer_Syntax.local_theory_to_proof "quotient_type"
--- a/src/HOL/Tools/SMT/smt_config.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Thu Mar 15 20:07:00 2012 +0100
@@ -86,7 +86,7 @@
context
|> Solvers.map (apfst (Symtab.update (name, (info, []))))
|> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
- (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (@{keyword "="} |-- Args.name) >>
(Thm.declaration_attribute o K o set_solver_options o pair name))
("Additional command line options for SMT solver " ^ quote name))
@@ -142,7 +142,7 @@
val setup_solver =
Attrib.setup @{binding smt_solver}
- (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (@{keyword "="} |-- Args.name) >>
(Thm.declaration_attribute o K o select_solver))
"SMT solver configuration"
@@ -207,7 +207,7 @@
val setup_certificates =
Attrib.setup @{binding smt_certificates}
- (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (@{keyword "="} |-- Args.name) >>
(Thm.declaration_attribute o K o select_certificates))
"SMT certificates configuration"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 15 20:07:00 2012 +0100
@@ -396,12 +396,12 @@
|> sort_strings |> cat_lines))
end))
-val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
+val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
val parse_key =
Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
val parse_value =
Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
-val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
val parse_fact_refs =
Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
--- a/src/HOL/Tools/choice_specification.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/choice_specification.ML Thu Mar 15 20:07:00 2012 +0100
@@ -234,11 +234,11 @@
(* outer syntax *)
-val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
+val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
val opt_overloaded = Parse.opt_keyword "overloaded"
val specification_decl =
- Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+ @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
val _ =
@@ -249,7 +249,7 @@
val ax_specification_decl =
Parse.name --
- (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+ (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
val _ =
--- a/src/HOL/Tools/enriched_type.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/enriched_type.ML Thu Mar 15 20:07:00 2012 +0100
@@ -268,7 +268,7 @@
val _ = Outer_Syntax.local_theory_to_proof "enriched_type"
"register operations managing the functorial structure of a type"
- Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
+ Keyword.thy_goal (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
>> (fn (prfx, t) => enriched_type_cmd prfx t));
end;
--- a/src/HOL/Tools/inductive.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Mar 15 20:07:00 2012 +0100
@@ -1137,7 +1137,7 @@
fun gen_ind_decl mk_def coind =
Parse.fixes -- Parse.for_fixes --
Scan.optional Parse_Spec.where_alt_specs [] --
- Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((preds, params), specs), monos) =>
(snd oo gen_add_inductive mk_def true coind preds params specs monos));
--- a/src/HOL/Tools/recdef.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/recdef.ML Thu Mar 15 20:07:00 2012 +0100
@@ -291,12 +291,12 @@
(* outer syntax *)
val hints =
- Parse.$$$ "(" |--
- Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
+ @{keyword "("} |--
+ Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src;
val recdef_decl =
Scan.optional
- (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
+ (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
-- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
@@ -309,7 +309,7 @@
val defer_recdef_decl =
Parse.name -- Scan.repeat1 Parse.prop --
Scan.optional
- (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
+ (@{keyword "("} |-- @{keyword "congs"} |-- Parse.!!! (Parse_Spec.xthms1 --| @{keyword ")"})) []
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
@@ -320,7 +320,7 @@
Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
Keyword.thy_goal
((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
- Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
+ Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
end;
--- a/src/HOL/Tools/record.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/record.ML Thu Mar 15 20:07:00 2012 +0100
@@ -2313,7 +2313,7 @@
val _ =
Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
(Parse.type_args_constrained -- Parse.binding --
- (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+ (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
--- a/src/HOL/Tools/refute.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/refute.ML Thu Mar 15 20:07:00 2012 +0100
@@ -3202,8 +3202,8 @@
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
-val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
+val scan_parm = Parse.name -- (Scan.optional (@{keyword "="} |-- Parse.name) "true")
+val scan_parms = Scan.optional (@{keyword "["} |-- Parse.list scan_parm --| @{keyword "]"}) [];
(* 'refute' command *)
--- a/src/HOL/Tools/typedef.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/typedef.ML Thu Mar 15 20:07:00 2012 +0100
@@ -302,12 +302,12 @@
val _ =
Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
Keyword.thy_goal
- (Scan.optional (Parse.$$$ "(" |--
- ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
- Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
+ (Scan.optional (@{keyword "("} |--
+ ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
(Parse.type_args_constrained -- Parse.binding) --
- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
>> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
--- a/src/Tools/Code/code_printer.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/Code/code_printer.ML Thu Mar 15 20:07:00 2012 +0100
@@ -394,13 +394,11 @@
| _ => Scan.!! (err s) Scan.fail ()
end;
-val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
-
fun parse_syntax mk_plain mk_complex prep_arg =
Scan.option (
- ((Parse.$$$ infixK >> K X)
- || (Parse.$$$ infixlK >> K L)
- || (Parse.$$$ infixrK >> K R))
+ ((@{keyword "infix"} >> K X)
+ || (@{keyword "infixl"} >> K L)
+ || (@{keyword "infixr"} >> K R))
-- Parse.nat -- Parse.string
>> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
|| Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
--- a/src/Tools/Code/code_runtime.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML Thu Mar 15 20:07:00 2012 +0100
@@ -344,24 +344,19 @@
local
-val datatypesK = "datatypes";
-val functionsK = "functions";
-val fileK = "file";
-val andK = "and"
-
val parse_datatype =
- Parse.name --| Parse.$$$ "=" --
+ Parse.name --| @{keyword "="} --
(((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
- || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
+ || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
in
val _ =
Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
- Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
- ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
- -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
- -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+ Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
+ ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
+ -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
+ -- Scan.option (@{keyword "file"} |-- Parse.name)
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
(code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
--- a/src/Tools/Code/code_target.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/Code/code_target.ML Thu Mar 15 20:07:00 2012 +0100
@@ -638,8 +638,8 @@
fun process_multi_syntax parse_thing parse_syntax change =
(Parse.and_list1 parse_thing
- :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
- (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
+ :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
+ (zip_list things parse_syntax (@{keyword "and"})) --| @{keyword ")"})))
>> (Toplevel.theory oo fold)
(fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
@@ -667,18 +667,16 @@
(** Isar setup **)
-val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking");
-
-val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [];
+val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
val code_exprP =
Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
- ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name
- -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
+ ((@{keyword "checking"} |-- Scan.repeat (Parse.name
+ -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
>> (fn seris => check_code_cmd raw_cs seris)
- || Scan.repeat (Parse.$$$ inK |-- Parse.name
- -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
- -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
+ || Scan.repeat (@{keyword "in"} |-- Parse.name
+ -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
+ -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
-- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
val _ =
@@ -688,7 +686,7 @@
val _ =
Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
- process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+ process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
add_instance_syntax_cmd);
@@ -713,7 +711,7 @@
Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
Keyword.thy_decl (
Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
- | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
+ | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
>> (fn ((target, name), content_consts) =>
(Toplevel.theory o add_include_cmd target) (name, content_consts))
);
--- a/src/Tools/interpretation_with_defs.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML Thu Mar 15 20:07:00 2012 +0100
@@ -83,8 +83,8 @@
Outer_Syntax.command "interpretation"
"prove interpretation of locale expression in theory" Keyword.thy_goal
(Parse.!!! (Parse_Spec.locale_expression true) --
- Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
- -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
+ Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
>> (fn ((expr, defs), equations) => Toplevel.print o
Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
--- a/src/Tools/quickcheck.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/quickcheck.ML Thu Mar 15 20:07:00 2012 +0100
@@ -522,12 +522,12 @@
val parse_arg =
Parse.name --
- (Scan.optional (Parse.$$$ "=" |--
+ (Scan.optional (@{keyword "="} |--
(((Parse.name || Parse.float_number) >> single) ||
- (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
+ (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}))) ["true"]);
val parse_args =
- Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
+ @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
val _ =
Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
--- a/src/Tools/value.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/value.ML Thu Mar 15 20:07:00 2012 +0100
@@ -57,10 +57,10 @@
in Pretty.writeln p end;
val opt_modes =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val opt_evaluator =
- Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]")
+ Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
val _ =
Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
--- a/src/ZF/Tools/datatype_package.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/ZF/Tools/datatype_package.ML Thu Mar 15 20:07:00 2012 +0100
@@ -427,15 +427,15 @@
#1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
val con_decl =
- Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
+ Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
Parse.opt_mixfix >> Parse.triple1;
val datatype_decl =
- (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
- Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
- Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
+ (Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
+ Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_datatype);
val coind_prefix = if coind then "co" else "";
--- a/src/ZF/Tools/induct_tacs.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Thu Mar 15 20:07:00 2012 +0100
@@ -189,10 +189,10 @@
(* outer syntax *)
val rep_datatype_decl =
- (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
- (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
- (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
- Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
+ (@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
+ (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
+ (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
+ Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((x, y), z), w) => rep_datatype x y z w);
val _ =
--- a/src/ZF/Tools/inductive_package.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/ZF/Tools/inductive_package.ML Thu Mar 15 20:07:00 2012 +0100
@@ -580,14 +580,14 @@
#1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
val ind_decl =
- (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
- ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
- (Parse.$$$ "intros" |--
+ (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term --
+ ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
+ (@{keyword "intros"} |--
Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
- Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_ind);
val _ =