1.1 --- a/NEWS Sat Oct 06 16:41:22 2007 +0200
1.2 +++ b/NEWS Sat Oct 06 16:50:04 2007 +0200
1.3 @@ -1337,6 +1337,11 @@
1.4 quasi-functional intermediate checkpoint, both in interactive and
1.5 batch mode.
1.6
1.7 +* Isar: simplified interfaces for outer syntax. Renamed
1.8 +OuterSyntax.add_keywords to OuterSyntax.keywords. Removed
1.9 +OuterSyntax.add_parsers -- this functionality is now included in
1.10 +OuterSyntax.command etc. INCOMPATIBILITY.
1.11 +
1.12 * Simplifier: the simpset of a running simplification process now
1.13 contains a proof context (cf. Simplifier.the_context), which is the
1.14 very context that the initial simpset has been retrieved from (by
2.1 --- a/src/HOL/Import/import_syntax.ML Sat Oct 06 16:41:22 2007 +0200
2.2 +++ b/src/HOL/Import/import_syntax.ML Sat Oct 06 16:50:04 2007 +0200
2.3 @@ -5,7 +5,7 @@
2.4
2.5 signature HOL4_IMPORT_SYNTAX =
2.6 sig
2.7 - type token = OuterSyntax.token
2.8 + type token = OuterLex.token
2.9 type command = token list -> (theory -> theory) * token list
2.10
2.11 val import_segment: token list -> (theory -> theory) * token list
2.12 @@ -32,7 +32,7 @@
2.13 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
2.14 struct
2.15
2.16 -type token = OuterSyntax.token
2.17 +type token = OuterLex.token
2.18 type command = token list -> (theory -> theory) * token list
2.19
2.20 local structure P = OuterParse and K = OuterKeyword in
2.21 @@ -222,61 +222,59 @@
2.22 fun fl_dump toks = Scan.succeed flush_dump toks
2.23 val append_dump = (P.verbatim || P.string) >> add_dump
2.24
2.25 -val parsers =
2.26 - [OuterSyntax.command "import_segment"
2.27 +fun setup () =
2.28 + (OuterSyntax.keywords[">"];
2.29 + OuterSyntax.command "import_segment"
2.30 "Set import segment name"
2.31 - K.thy_decl (import_segment >> Toplevel.theory),
2.32 + K.thy_decl (import_segment >> Toplevel.theory);
2.33 OuterSyntax.command "import_theory"
2.34 "Set default HOL4 theory name"
2.35 - K.thy_decl (import_theory >> Toplevel.theory),
2.36 + K.thy_decl (import_theory >> Toplevel.theory);
2.37 OuterSyntax.command "end_import"
2.38 "End HOL4 import"
2.39 - K.thy_decl (end_import >> Toplevel.theory),
2.40 + K.thy_decl (end_import >> Toplevel.theory);
2.41 OuterSyntax.command "skip_import_dir"
2.42 "Sets caching directory for skipping importing"
2.43 - K.thy_decl (skip_import_dir >> Toplevel.theory),
2.44 + K.thy_decl (skip_import_dir >> Toplevel.theory);
2.45 OuterSyntax.command "skip_import"
2.46 "Switches skipping importing on or off"
2.47 - K.thy_decl (skip_import >> Toplevel.theory),
2.48 + K.thy_decl (skip_import >> Toplevel.theory);
2.49 OuterSyntax.command "setup_theory"
2.50 "Setup HOL4 theory replaying"
2.51 - K.thy_decl (setup_theory >> Toplevel.theory),
2.52 + K.thy_decl (setup_theory >> Toplevel.theory);
2.53 OuterSyntax.command "end_setup"
2.54 "End HOL4 setup"
2.55 - K.thy_decl (end_setup >> Toplevel.theory),
2.56 + K.thy_decl (end_setup >> Toplevel.theory);
2.57 OuterSyntax.command "setup_dump"
2.58 "Setup the dump file name"
2.59 - K.thy_decl (set_dump >> Toplevel.theory),
2.60 + K.thy_decl (set_dump >> Toplevel.theory);
2.61 OuterSyntax.command "append_dump"
2.62 "Add text to dump file"
2.63 - K.thy_decl (append_dump >> Toplevel.theory),
2.64 + K.thy_decl (append_dump >> Toplevel.theory);
2.65 OuterSyntax.command "flush_dump"
2.66 "Write the dump to file"
2.67 - K.thy_decl (fl_dump >> Toplevel.theory),
2.68 + K.thy_decl (fl_dump >> Toplevel.theory);
2.69 OuterSyntax.command "ignore_thms"
2.70 "Theorems to ignore in next HOL4 theory import"
2.71 - K.thy_decl (ignore_thms >> Toplevel.theory),
2.72 + K.thy_decl (ignore_thms >> Toplevel.theory);
2.73 OuterSyntax.command "type_maps"
2.74 "Map HOL4 type names to existing Isabelle/HOL type names"
2.75 - K.thy_decl (type_maps >> Toplevel.theory),
2.76 + K.thy_decl (type_maps >> Toplevel.theory);
2.77 OuterSyntax.command "def_maps"
2.78 "Map HOL4 constant names to their primitive definitions"
2.79 - K.thy_decl (def_maps >> Toplevel.theory),
2.80 + K.thy_decl (def_maps >> Toplevel.theory);
2.81 OuterSyntax.command "thm_maps"
2.82 "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
2.83 - K.thy_decl (thm_maps >> Toplevel.theory),
2.84 + K.thy_decl (thm_maps >> Toplevel.theory);
2.85 OuterSyntax.command "const_renames"
2.86 "Rename HOL4 const names"
2.87 - K.thy_decl (const_renames >> Toplevel.theory),
2.88 + K.thy_decl (const_renames >> Toplevel.theory);
2.89 OuterSyntax.command "const_moves"
2.90 "Rename HOL4 const names to other HOL4 constants"
2.91 - K.thy_decl (const_moves >> Toplevel.theory),
2.92 + K.thy_decl (const_moves >> Toplevel.theory);
2.93 OuterSyntax.command "const_maps"
2.94 "Map HOL4 const names to existing Isabelle/HOL const names"
2.95 - K.thy_decl (const_maps >> Toplevel.theory)]
2.96 -
2.97 -fun setup () = (OuterSyntax.add_keywords[">"];
2.98 - OuterSyntax.add_parsers parsers)
2.99 + K.thy_decl (const_maps >> Toplevel.theory));
2.100
2.101 end
2.102
3.1 --- a/src/HOL/Library/Eval.thy Sat Oct 06 16:41:22 2007 +0200
3.2 +++ b/src/HOL/Library/Eval.thy Sat Oct 06 16:50:04 2007 +0200
3.3 @@ -213,14 +213,11 @@
3.4 *}
3.5
3.6 ML {*
3.7 -val valueP =
3.8 OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
3.9 (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
3.10 -- OuterParse.term
3.11 >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
3.12 (Eval.evaluate_cmd some_name t)));
3.13 -
3.14 -val _ = OuterSyntax.add_parsers [valueP];
3.15 *}
3.16
3.17 end
4.1 --- a/src/HOL/Nominal/nominal_atoms.ML Sat Oct 06 16:41:22 2007 +0200
4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Oct 06 16:50:04 2007 +0200
4.3 @@ -947,10 +947,8 @@
4.4 (* syntax und parsing *)
4.5 structure P = OuterParse and K = OuterKeyword;
4.6
4.7 -val atom_declP =
4.8 +val _ =
4.9 OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
4.10 (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
4.11
4.12 -val _ = OuterSyntax.add_parsers [atom_declP];
4.13 -
4.14 end;
5.1 --- a/src/HOL/Nominal/nominal_inductive.ML Sat Oct 06 16:41:22 2007 +0200
5.2 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Oct 06 16:50:04 2007 +0200
5.3 @@ -511,22 +511,21 @@
5.4
5.5 local structure P = OuterParse and K = OuterKeyword in
5.6
5.7 -val nominal_inductiveP =
5.8 +val _ = OuterSyntax.keywords ["avoids"];
5.9 +
5.10 +val _ =
5.11 OuterSyntax.command "nominal_inductive"
5.12 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
5.13 (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
5.14 (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
5.15 Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
5.16
5.17 -val equivarianceP =
5.18 +val _ =
5.19 OuterSyntax.command "equivariance"
5.20 "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
5.21 (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
5.22 (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
5.23
5.24 -val _ = OuterSyntax.add_keywords ["avoids"];
5.25 -val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];
5.26 -
5.27 end;
5.28
5.29 end
6.1 --- a/src/HOL/Nominal/nominal_package.ML Sat Oct 06 16:41:22 2007 +0200
6.2 +++ b/src/HOL/Nominal/nominal_package.ML Sat Oct 06 16:50:04 2007 +0200
6.3 @@ -2094,12 +2094,10 @@
6.4 (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
6.5 in add_nominal_datatype false names specs end;
6.6
6.7 -val nominal_datatypeP =
6.8 +val _ =
6.9 OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
6.10 (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
6.11
6.12 -val _ = OuterSyntax.add_parsers [nominal_datatypeP];
6.13 -
6.14 end;
6.15
6.16 end
7.1 --- a/src/HOL/Nominal/nominal_primrec.ML Sat Oct 06 16:41:22 2007 +0200
7.2 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Oct 06 16:50:04 2007 +0200
7.3 @@ -416,6 +416,8 @@
7.4
7.5 local structure P = OuterParse and K = OuterKeyword in
7.6
7.7 +val _ = OuterSyntax.keywords ["invariant", "freshness_context"];
7.8 +
7.9 val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
7.10 val parser2 =
7.11 P.$$$ "invariant" |-- P.$$$ ":" |--
7.12 @@ -434,18 +436,15 @@
7.13 val primrec_decl =
7.14 options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
7.15
7.16 -val primrecP =
7.17 +val _ =
7.18 OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
7.19 (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
7.20 Toplevel.print o Toplevel.theory_to_proof
7.21 ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
7.22 (map P.triple_swap eqns))));
7.23
7.24 -val _ = OuterSyntax.add_parsers [primrecP];
7.25 -val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
7.26 +end;
7.27 +
7.28
7.29 end;
7.30
7.31 -
7.32 -end;
7.33 -
8.1 --- a/src/HOL/Orderings.thy Sat Oct 06 16:41:22 2007 +0200
8.2 +++ b/src/HOL/Orderings.thy Sat Oct 06 16:50:04 2007 +0200
8.3 @@ -346,7 +346,7 @@
8.4 (Context.cases (print_structures o ProofContext.init) print_structures)
8.5 (print_structures o Proof.context_of));
8.6
8.7 -val printP =
8.8 +val _ =
8.9 OuterSyntax.improper_command "print_orders"
8.10 "print order structures available to transitivity reasoner" OuterKeyword.diag
8.11 (Scan.succeed (Toplevel.no_timing o print));
8.12 @@ -354,11 +354,10 @@
8.13
8.14 (** Setup **)
8.15
8.16 -val setup = let val _ = OuterSyntax.add_parsers [printP] in
8.17 - Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
8.18 - "normalisation of algebraic structure")] #>
8.19 - Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
8.20 - end;
8.21 +val setup =
8.22 + Method.add_methods
8.23 + [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
8.24 + Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
8.25
8.26 end;
8.27
9.1 --- a/src/HOL/Tools/datatype_package.ML Sat Oct 06 16:41:22 2007 +0200
9.2 +++ b/src/HOL/Tools/datatype_package.ML Sat Oct 06 16:50:04 2007 +0200
9.3 @@ -908,6 +908,8 @@
9.4
9.5 local structure P = OuterParse and K = OuterKeyword in
9.6
9.7 +val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
9.8 +
9.9 val datatype_decl =
9.10 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
9.11 (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
9.12 @@ -919,7 +921,7 @@
9.13 (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
9.14 in snd o add_datatype false names specs end;
9.15
9.16 -val datatypeP =
9.17 +val _ =
9.18 OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
9.19 (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
9.20
9.21 @@ -932,14 +934,10 @@
9.22
9.23 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
9.24
9.25 -val rep_datatypeP =
9.26 +val _ =
9.27 OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
9.28 (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
9.29
9.30 -
9.31 -val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
9.32 -val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
9.33 -
9.34 end;
9.35
9.36
10.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML Sat Oct 06 16:41:22 2007 +0200
10.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Sat Oct 06 16:50:04 2007 +0200
10.3 @@ -302,13 +302,12 @@
10.4 |> by_pat_completeness_simp
10.5 |> termination_by_lexicographic_order
10.6
10.7 -val funP =
10.8 +val _ =
10.9 OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
10.10 (fundef_parser fun_config
10.11 >> (fn ((config, fixes), (flags, statements)) =>
10.12 (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
10.13
10.14 -val _ = OuterSyntax.add_parsers [funP];
10.15 end
10.16
10.17 end
11.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 06 16:41:22 2007 +0200
11.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 06 16:50:04 2007 +0200
11.3 @@ -268,24 +268,22 @@
11.4
11.5 local structure P = OuterParse and K = OuterKeyword in
11.6
11.7 -val functionP =
11.8 +val _ = OuterSyntax.keywords ["sequential", "otherwise"];
11.9 +
11.10 +val _ =
11.11 OuterSyntax.command "function" "define general recursive functions" K.thy_goal
11.12 (fundef_parser default_config
11.13 >> (fn ((config, fixes), (flags, statements)) =>
11.14 Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
11.15 #> Toplevel.print));
11.16
11.17 -val terminationP =
11.18 +val _ =
11.19 OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
11.20 (P.opt_target -- Scan.option P.term
11.21 >> (fn (target, name) =>
11.22 Toplevel.print o
11.23 Toplevel.local_theory_to_proof target (setup_termination_proof name)));
11.24
11.25 -val _ = OuterSyntax.add_parsers [functionP];
11.26 -val _ = OuterSyntax.add_parsers [terminationP];
11.27 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
11.28 -
11.29 end;
11.30
11.31
12.1 --- a/src/HOL/Tools/inductive_package.ML Sat Oct 06 16:41:22 2007 +0200
12.2 +++ b/src/HOL/Tools/inductive_package.ML Sat Oct 06 16:50:04 2007 +0200
12.3 @@ -923,6 +923,8 @@
12.4
12.5 local structure P = OuterParse and K = OuterKeyword in
12.6
12.7 +val _ = OuterSyntax.keywords ["monos"];
12.8 +
12.9 (* FIXME tmp *)
12.10 fun flatten_specification specs = specs |> maps
12.11 (fn (a, (concl, [])) => concl |> map
12.12 @@ -945,22 +947,15 @@
12.13
12.14 val ind_decl = gen_ind_decl add_ind_def;
12.15
12.16 -val inductiveP =
12.17 - OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
12.18 +val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
12.19 +val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
12.20
12.21 -val coinductiveP =
12.22 - OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
12.23 -
12.24 -
12.25 -val inductive_casesP =
12.26 +val _ =
12.27 OuterSyntax.command "inductive_cases"
12.28 "create simplified instances of elimination rules (improper)" K.thy_script
12.29 (P.opt_target -- P.and_list1 SpecParse.spec
12.30 >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
12.31
12.32 -val _ = OuterSyntax.add_keywords ["monos"];
12.33 -val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
12.34 -
12.35 end;
12.36
12.37 end;
13.1 --- a/src/HOL/Tools/inductive_set_package.ML Sat Oct 06 16:41:22 2007 +0200
13.2 +++ b/src/HOL/Tools/inductive_set_package.ML Sat Oct 06 16:50:04 2007 +0200
13.3 @@ -543,14 +543,12 @@
13.4
13.5 val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
13.6
13.7 -val inductive_setP =
13.8 +val _ =
13.9 OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
13.10
13.11 -val coinductive_setP =
13.12 +val _ =
13.13 OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
13.14
13.15 -val _ = OuterSyntax.add_parsers [inductive_setP, coinductive_setP];
13.16 -
13.17 end;
13.18
13.19 end;
14.1 --- a/src/HOL/Tools/primrec_package.ML Sat Oct 06 16:41:22 2007 +0200
14.2 +++ b/src/HOL/Tools/primrec_package.ML Sat Oct 06 16:50:04 2007 +0200
14.3 @@ -350,15 +350,13 @@
14.4 val primrec_decl =
14.5 opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
14.6
14.7 -val primrecP =
14.8 +val _ =
14.9 OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
14.10 (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
14.11 Toplevel.theory (snd o
14.12 (if unchecked then add_primrec_unchecked else add_primrec) alt_name
14.13 (map P.triple_swap eqns))));
14.14
14.15 -val _ = OuterSyntax.add_parsers [primrecP];
14.16 -
14.17 end;
14.18
14.19 end;
15.1 --- a/src/HOL/Tools/recdef_package.ML Sat Oct 06 16:41:22 2007 +0200
15.2 +++ b/src/HOL/Tools/recdef_package.ML Sat Oct 06 16:50:04 2007 +0200
15.3 @@ -295,6 +295,8 @@
15.4
15.5 local structure P = OuterParse and K = OuterKeyword in
15.6
15.7 +val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
15.8 +
15.9 val hints =
15.10 P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
15.11
15.12 @@ -303,7 +305,7 @@
15.13 P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
15.14 >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
15.15
15.16 -val recdefP =
15.17 +val _ =
15.18 OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
15.19 (recdef_decl >> Toplevel.theory);
15.20
15.21 @@ -313,21 +315,17 @@
15.22 Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
15.23 >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
15.24
15.25 -val defer_recdefP =
15.26 +val _ =
15.27 OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
15.28 (defer_recdef_decl >> Toplevel.theory);
15.29
15.30 -val recdef_tcP =
15.31 +val _ =
15.32 OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
15.33 (P.opt_target --
15.34 SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
15.35 >> (fn (((loc, thm_name), name), i) =>
15.36 Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
15.37
15.38 -
15.39 -val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
15.40 -val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
15.41 -
15.42 end;
15.43
15.44 end;
16.1 --- a/src/HOL/Tools/record_package.ML Sat Oct 06 16:41:22 2007 +0200
16.2 +++ b/src/HOL/Tools/record_package.ML Sat Oct 06 16:50:04 2007 +0200
16.3 @@ -607,7 +607,7 @@
16.4 val types = map snd flds';
16.5 val (args,rest) = splitargs (map fst flds') fargs;
16.6 val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
16.7 - val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
16.8 + val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
16.9 argtypes 0;
16.10 val varifyT = varifyT midx;
16.11 val vartypes = map varifyT types;
16.12 @@ -654,12 +654,12 @@
16.13 gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
16.14
16.15
16.16 -val parse_translation =
16.17 +val parse_translation =
16.18 [("_record_update", record_update_tr),
16.19 ("_update_name", update_name_tr)];
16.20
16.21
16.22 -val adv_parse_translation =
16.23 +val adv_parse_translation =
16.24 [("_record",adv_record_tr),
16.25 ("_record_scheme",adv_record_scheme_tr),
16.26 ("_record_type",adv_record_type_tr),
16.27 @@ -762,7 +762,7 @@
16.28 in Syntax.term_of_typ (! Syntax.show_sorts)
16.29 (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
16.30
16.31 - fun match rT T = (Sign.typ_match thy (varifyT rT,T)
16.32 + fun match rT T = (Sign.typ_match thy (varifyT rT,T)
16.33 Vartab.empty);
16.34
16.35 in if !print_record_type_abbr
16.36 @@ -876,8 +876,8 @@
16.37 val f_x = Free (f',fT)$(Free (x,T'));
16.38 fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
16.39 | is_constr _ = false;
16.40 - fun subst (t as u$w) = if Free (f',fT)=u
16.41 - then if is_constr w then f_x
16.42 + fun subst (t as u$w) = if Free (f',fT)=u
16.43 + then if is_constr w then f_x
16.44 else raise TERM ("abstract_over_fun_app",[t])
16.45 else subst u$subst w
16.46 | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
16.47 @@ -885,12 +885,12 @@
16.48 val t'' = abstract_over (f_x,subst t');
16.49 val vars = strip_qnt_vars "all" t'';
16.50 val bdy = strip_qnt_body "all" t'';
16.51 -
16.52 +
16.53 in list_abs ((x,T')::vars,bdy) end
16.54 | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
16.55 (* Generates a theorem of the kind:
16.56 - * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
16.57 - *)
16.58 + * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
16.59 + *)
16.60 fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
16.61 let
16.62 val rT = domain_type fT;
16.63 @@ -900,16 +900,16 @@
16.64 fun app_bounds 0 t = t$Bound 0
16.65 | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
16.66
16.67 -
16.68 +
16.69 val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
16.70 val prop = Logic.mk_equals
16.71 (list_all ((f,fT)::vars,
16.72 app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
16.73 list_all ((fst r,rT)::vars,
16.74 - app_bounds (n - 1) ((Free P)$Bound n)));
16.75 + app_bounds (n - 1) ((Free P)$Bound n)));
16.76 val prove_standard = quick_and_dirty_prove true thy;
16.77 val thm = prove_standard [] prop (fn prems =>
16.78 - EVERY [rtac equal_intr_rule 1,
16.79 + EVERY [rtac equal_intr_rule 1,
16.80 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
16.81 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
16.82 in thm end
16.83 @@ -928,14 +928,14 @@
16.84 (trm as Abs _) =>
16.85 (case rec_id (~1) T of
16.86 "" => NONE
16.87 - | n => if T=T'
16.88 + | n => if T=T'
16.89 then (let
16.90 - val P=cterm_of thy (abstract_over_fun_app trm);
16.91 + val P=cterm_of thy (abstract_over_fun_app trm);
16.92 val thm = mk_fun_apply_eq trm thy;
16.93 val PV = cterm_of thy (hd (term_vars (prop_of thm)));
16.94 val thm' = cterm_instantiate [(PV,P)] thm;
16.95 in SOME thm' end handle TERM _ => NONE)
16.96 - else NONE)
16.97 + else NONE)
16.98 | _ => NONE))
16.99 end
16.100
16.101 @@ -951,7 +951,7 @@
16.102 (* [thm] is the same as all_thm *)
16.103 | NONE => extsplits)
16.104 val thms'=K_comp_convs@thms;
16.105 - val ss' = (Simplifier.inherit_context ss simpset
16.106 + val ss' = (Simplifier.inherit_context ss simpset
16.107 addsimps thms'
16.108 addsimprocs [record_split_f_more_simproc]);
16.109 in
16.110 @@ -992,8 +992,8 @@
16.111 NONE => NONE
16.112 | SOME u_name
16.113 => if u_name = s
16.114 - then (case mk_eq_terms r of
16.115 - NONE =>
16.116 + then (case mk_eq_terms r of
16.117 + NONE =>
16.118 let
16.119 val rv = ("r",rT)
16.120 val rb = Bound 0
16.121 @@ -1064,7 +1064,7 @@
16.122 in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
16.123 else ((sprout,skeleton),vars);
16.124
16.125 - fun is_upd_same (sprout,skeleton) u
16.126 + fun is_upd_same (sprout,skeleton) u
16.127 ((K_rec as Const ("Record.K_record",_))$
16.128 ((sel as Const (s,_))$r)) =
16.129 if (unsuffix updateN u) = s andalso (seed s sprout) = r
16.130 @@ -1074,17 +1074,17 @@
16.131
16.132 fun init_seed r = ((r,Bound 0), [("r", rT)]);
16.133
16.134 - fun add (n:string) f fmaps =
16.135 + fun add (n:string) f fmaps =
16.136 (case AList.lookup (op =) fmaps n of
16.137 NONE => AList.update (op =) (n,[f]) fmaps
16.138 - | SOME fs => AList.update (op =) (n,f::fs) fmaps)
16.139 + | SOME fs => AList.update (op =) (n,f::fs) fmaps)
16.140
16.141 - fun comps (n:string) T fmaps =
16.142 + fun comps (n:string) T fmaps =
16.143 (case AList.lookup (op =) fmaps n of
16.144 - SOME fs =>
16.145 + SOME fs =>
16.146 foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
16.147 | NONE => error ("record_upd_simproc.comps"))
16.148 -
16.149 +
16.150 (* mk_updterm returns either
16.151 * - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
16.152 * where vars are the bound variables in the skeleton
16.153 @@ -1119,7 +1119,7 @@
16.154 val kv = (n, kT);
16.155 val kb = Bound (length vars);
16.156 val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
16.157 - in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
16.158 + in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
16.159 end)
16.160 else
16.161 (case rest (u::already) r of
16.162 @@ -1149,7 +1149,7 @@
16.163 val kv = (n, kT)
16.164 val kb = Bound (length vars)
16.165 val (sprout',vars') = grow u uT k kT (kv::vars) sprout
16.166 - val fmaps' = add n kb fmaps
16.167 + val fmaps' = add n kb fmaps
16.168 in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
16.169 ,vars',fmaps',sprout') end))
16.170 end
16.171 @@ -1161,7 +1161,7 @@
16.172 => SOME (prove_split_simp thy ss rT
16.173 (list_all(vars,(equals rT$trm$trm'))))
16.174 | _ => NONE)
16.175 - end
16.176 + end
16.177 | _ => NONE))
16.178 end
16.179
16.180 @@ -1625,7 +1625,7 @@
16.181 val refls = map mkrefl fields_more;
16.182 val dest_convs' = map mk_meta_eq dest_convs;
16.183 val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
16.184 -
16.185 +
16.186 val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
16.187
16.188 fun mkthm (udef,(fld_refl,thms)) =
16.189 @@ -1664,7 +1664,7 @@
16.190 val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
16.191
16.192
16.193 - val (([inject',induct',cases',surjective',split_meta'],
16.194 + val (([inject',induct',cases',surjective',split_meta'],
16.195 [dest_convs',upd_convs']),
16.196 thm_thy) =
16.197 defs_thy
16.198 @@ -1915,7 +1915,7 @@
16.199 ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
16.200 ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
16.201 [make_spec, fields_spec, extend_spec, truncate_spec])
16.202 - |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
16.203 + |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
16.204 fold Code.add_default_func sel_defs
16.205 #> fold Code.add_default_func upd_defs
16.206 #> fold Code.add_default_func derived_defs
16.207 @@ -2276,12 +2276,10 @@
16.208 P.type_args -- P.name --
16.209 (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
16.210
16.211 -val recordP =
16.212 +val _ =
16.213 OuterSyntax.command "record" "define extensible record" K.thy_decl
16.214 (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
16.215
16.216 -val _ = OuterSyntax.add_parsers [recordP];
16.217 -
16.218 end;
16.219
16.220 end;
17.1 --- a/src/HOL/Tools/refute_isar.ML Sat Oct 06 16:41:22 2007 +0200
17.2 +++ b/src/HOL/Tools/refute_isar.ML Sat Oct 06 16:50:04 2007 +0200
17.3 @@ -7,7 +7,7 @@
17.4 syntax.
17.5 *)
17.6
17.7 -structure RefuteIsar =
17.8 +structure RefuteIsar: sig end =
17.9 struct
17.10
17.11 (* ------------------------------------------------------------------------- *)
17.12 @@ -56,7 +56,7 @@
17.13
17.14 fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
17.15
17.16 - val refute_cmd = OuterSyntax.improper_command "refute"
17.17 + val _ = OuterSyntax.improper_command "refute"
17.18 "try to find a model that refutes a given subgoal"
17.19 OuterKeyword.diag refute_parser;
17.20
17.21 @@ -101,15 +101,9 @@
17.22 fun refute_params_parser tokens =
17.23 (refute_params_scan_args tokens) |>> refute_params_trans;
17.24
17.25 - val refute_params_cmd = OuterSyntax.command "refute_params"
17.26 + val _ = OuterSyntax.command "refute_params"
17.27 "show/store default parameters for the 'refute' command"
17.28 OuterKeyword.thy_decl refute_params_parser;
17.29
17.30 end;
17.31
17.32 -(* ------------------------------------------------------------------------- *)
17.33 -(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's *)
17.34 -(* outer syntax *)
17.35 -(* ------------------------------------------------------------------------- *)
17.36 -
17.37 -OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];
18.1 --- a/src/HOL/Tools/res_atp.ML Sat Oct 06 16:41:22 2007 +0200
18.2 +++ b/src/HOL/Tools/res_atp.ML Sat Oct 06 16:50:04 2007 +0200
18.3 @@ -969,8 +969,8 @@
18.4 isar_atp_writeonly (ctxt, chain_ths, goal))
18.5 end;
18.6
18.7 -val _ = OuterSyntax.add_parsers
18.8 - [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
18.9 - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
18.10 +val _ =
18.11 + OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
18.12 + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
18.13
18.14 end;
19.1 --- a/src/HOL/Tools/specification_package.ML Sat Oct 06 16:41:22 2007 +0200
19.2 +++ b/src/HOL/Tools/specification_package.ML Sat Oct 06 16:50:04 2007 +0200
19.3 @@ -244,7 +244,7 @@
19.4 P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
19.5 Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
19.6
19.7 -val specificationP =
19.8 +val _ =
19.9 OuterSyntax.command "specification" "define constants by specification" K.thy_goal
19.10 (specification_decl >> (fn (cos,alt_props) =>
19.11 Toplevel.print o (Toplevel.theory_to_proof
19.12 @@ -255,15 +255,13 @@
19.13 (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
19.14 Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
19.15
19.16 -val ax_specificationP =
19.17 +val _ =
19.18 OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
19.19 (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
19.20 Toplevel.print o (Toplevel.theory_to_proof
19.21 (process_spec (SOME axname) cos alt_props))))
19.22
19.23 -val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]
19.24 +end
19.25 +
19.26
19.27 end
19.28 -
19.29 -
19.30 -end
20.1 --- a/src/HOL/Tools/typedef_package.ML Sat Oct 06 16:41:22 2007 +0200
20.2 +++ b/src/HOL/Tools/typedef_package.ML Sat Oct 06 16:50:04 2007 +0200
20.3 @@ -273,7 +273,9 @@
20.4
20.5 local structure P = OuterParse and K = OuterKeyword in
20.6
20.7 -val typedeclP =
20.8 +val _ = OuterSyntax.keywords ["morphisms"];
20.9 +
20.10 +val _ =
20.11 OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
20.12 (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
20.13 Toplevel.theory (add_typedecls [(t, vs, mx)])));
20.14 @@ -289,14 +291,10 @@
20.15 fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
20.16 typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
20.17
20.18 -val typedefP =
20.19 +val _ =
20.20 OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
20.21 (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
20.22
20.23 -
20.24 -val _ = OuterSyntax.add_keywords ["morphisms"];
20.25 -val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
20.26 -
20.27 end;
20.28
20.29 end;
21.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Oct 06 16:41:22 2007 +0200
21.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Oct 06 16:50:04 2007 +0200
21.3 @@ -481,10 +481,15 @@
21.4 add_rename aut source_aut rename_f;
21.5
21.6
21.7 -(* parsers *)
21.8 +(* outer syntax *)
21.9
21.10 local structure P = OuterParse and K = OuterKeyword in
21.11
21.12 +val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
21.13 + "outputs", "internals", "states", "initially", "transitions", "pre",
21.14 + "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
21.15 + "rename"];
21.16 +
21.17 val actionlist = P.list1 P.term;
21.18 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
21.19 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
21.20 @@ -520,21 +525,10 @@
21.21 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
21.22 >> mk_rename_decl;
21.23
21.24 -val automatonP =
21.25 +val _ =
21.26 OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
21.27 (ioa_decl >> Toplevel.theory);
21.28
21.29 end;
21.30
21.31 -
21.32 -(* setup outer syntax *)
21.33 -
21.34 -val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
21.35 - "outputs", "internals", "states", "initially", "transitions", "pre",
21.36 - "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
21.37 - "rename"];
21.38 -
21.39 -val _ = OuterSyntax.add_parsers [automatonP];
21.40 -
21.41 -
21.42 end;
22.1 --- a/src/HOLCF/Tools/cont_consts.ML Sat Oct 06 16:41:22 2007 +0200
22.2 +++ b/src/HOLCF/Tools/cont_consts.ML Sat Oct 06 16:50:04 2007 +0200
22.3 @@ -99,12 +99,10 @@
22.4
22.5 local structure P = OuterParse and K = OuterKeyword in
22.6
22.7 -val constsP =
22.8 +val _ =
22.9 OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
22.10 (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
22.11
22.12 -val _ = OuterSyntax.add_parsers [constsP];
22.13 -
22.14 end;
22.15
22.16 end;
23.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML Sat Oct 06 16:41:22 2007 +0200
23.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat Oct 06 16:50:04 2007 +0200
23.3 @@ -146,6 +146,8 @@
23.4
23.5 local structure P = OuterParse and K = OuterKeyword in
23.6
23.7 +val _ = OuterSyntax.keywords ["lazy"];
23.8 +
23.9 val dest_decl =
23.10 P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
23.11 (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
23.12 @@ -170,14 +172,10 @@
23.13 >> (fn (opt_name, doms) =>
23.14 (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
23.15
23.16 -val domainP =
23.17 +val _ =
23.18 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
23.19 (domains_decl >> (Toplevel.theory o add_domain));
23.20
23.21 -
23.22 -val _ = OuterSyntax.add_keywords ["lazy"];
23.23 -val _ = OuterSyntax.add_parsers [domainP];
23.24 -
23.25 -end; (* local structure *)
23.26 +end;
23.27
23.28 end;
24.1 --- a/src/HOLCF/Tools/fixrec_package.ML Sat Oct 06 16:41:22 2007 +0200
24.2 +++ b/src/HOLCF/Tools/fixrec_package.ML Sat Oct 06 16:50:04 2007 +0200
24.3 @@ -299,19 +299,17 @@
24.4
24.5 (* this builds a parser for a new keyword, fixrec, whose functionality
24.6 is defined by add_fixrec *)
24.7 -val fixrecP =
24.8 +val _ =
24.9 OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
24.10 (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
24.11
24.12 (* fixpat parser *)
24.13 val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
24.14
24.15 -val fixpatP =
24.16 +val _ =
24.17 OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
24.18 (fixpat_decl >> (Toplevel.theory o add_fixpat));
24.19
24.20 -val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
24.21 +end;
24.22
24.23 -end; (* local structure *)
24.24 -
24.25 -end; (* struct *)
24.26 +end;
25.1 --- a/src/HOLCF/Tools/pcpodef_package.ML Sat Oct 06 16:41:22 2007 +0200
25.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML Sat Oct 06 16:50:04 2007 +0200
25.3 @@ -184,7 +184,7 @@
25.4
25.5 local structure P = OuterParse and K = OuterKeyword in
25.6
25.7 -(* copied from HOL/Tools/typedef_package.ML *)
25.8 +(* cf. HOL/Tools/typedef_package.ML *)
25.9 val typedef_proof_decl =
25.10 Scan.optional (P.$$$ "(" |--
25.11 ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
25.12 @@ -196,18 +196,16 @@
25.13 (if pcpo then pcpodef_proof else cpodef_proof)
25.14 ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
25.15
25.16 -val pcpodefP =
25.17 +val _ =
25.18 OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
25.19 (typedef_proof_decl >>
25.20 (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
25.21
25.22 -val cpodefP =
25.23 +val _ =
25.24 OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
25.25 (typedef_proof_decl >>
25.26 (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
25.27
25.28 -val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
25.29 -
25.30 end;
25.31
25.32 end;
26.1 --- a/src/Provers/classical.ML Sat Oct 06 16:41:22 2007 +0200
26.2 +++ b/src/Provers/classical.ML Sat Oct 06 16:50:04 2007 +0200
26.3 @@ -1084,7 +1084,7 @@
26.4
26.5 (** outer syntax **)
26.6
26.7 -val print_clasetP =
26.8 +val _ =
26.9 OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
26.10 OuterKeyword.diag
26.11 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
26.12 @@ -1092,7 +1092,4 @@
26.13 (Context.cases print_claset print_local_claset)
26.14 (print_local_claset o Proof.context_of)))));
26.15
26.16 -val _ = OuterSyntax.add_parsers [print_clasetP];
26.17 -
26.18 -
26.19 end;
27.1 --- a/src/Pure/Proof/extraction.ML Sat Oct 06 16:41:22 2007 +0200
27.2 +++ b/src/Pure/Proof/extraction.ML Sat Oct 06 16:50:04 2007 +0200
27.3 @@ -759,7 +759,7 @@
27.4
27.5 val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
27.6
27.7 -val realizersP =
27.8 +val _ =
27.9 OuterSyntax.command "realizers"
27.10 "specify realizers for primitive axioms / theorems, together with correctness proof"
27.11 K.thy_decl
27.12 @@ -768,23 +768,21 @@
27.13 (map (fn (((a, vs), s1), s2) =>
27.14 (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
27.15
27.16 -val realizabilityP =
27.17 +val _ =
27.18 OuterSyntax.command "realizability"
27.19 "add equations characterizing realizability" K.thy_decl
27.20 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
27.21
27.22 -val typeofP =
27.23 +val _ =
27.24 OuterSyntax.command "extract_type"
27.25 "add equations characterizing type of extracted program" K.thy_decl
27.26 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
27.27
27.28 -val extractP =
27.29 +val _ =
27.30 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
27.31 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
27.32 (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
27.33
27.34 -val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
27.35 -
27.36 val etype_of = etype_of o add_syntax;
27.37
27.38 end;
28.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Oct 06 16:41:22 2007 +0200
28.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Oct 06 16:50:04 2007 +0200
28.3 @@ -231,36 +231,36 @@
28.4
28.5 local structure P = OuterParse and K = OuterKeyword in
28.6
28.7 -val undoP = (*undo without output*)
28.8 +fun undoP () = (*undo without output*)
28.9 OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
28.10 (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
28.11
28.12 -val restartP =
28.13 +fun restartP () =
28.14 OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
28.15 (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
28.16
28.17 -val kill_proofP =
28.18 +fun kill_proofP () =
28.19 OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
28.20 (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
28.21
28.22 -val inform_file_processedP =
28.23 +fun inform_file_processedP () =
28.24 OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
28.25 (P.name >> (fn file => Toplevel.no_timing o
28.26 Toplevel.init_empty (vacuous_inform_file_processed file) o
28.27 Toplevel.kill o
28.28 Toplevel.init_empty (proper_inform_file_processed file)));
28.29
28.30 -val inform_file_retractedP =
28.31 +fun inform_file_retractedP () =
28.32 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
28.33 (P.name >> (Toplevel.no_timing oo
28.34 (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
28.35
28.36 -val process_pgipP =
28.37 +fun process_pgipP () =
28.38 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
28.39 (P.text >> (Toplevel.no_timing oo
28.40 (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
28.41
28.42 -fun init_outer_syntax () = OuterSyntax.add_parsers
28.43 +fun init_outer_syntax () = List.app (fn f => f ())
28.44 [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
28.45
28.46 end;
29.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Oct 06 16:41:22 2007 +0200
29.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Oct 06 16:50:04 2007 +0200
29.3 @@ -1125,21 +1125,13 @@
29.4 end
29.5
29.6
29.7 -local
29.8 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
29.9
29.10 -val process_pgipP =
29.11 +fun init_outer_syntax () =
29.12 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
29.13 (OuterParse.text >> (Toplevel.no_timing oo
29.14 (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
29.15
29.16 -in
29.17 -
29.18 - fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
29.19 -
29.20 -end
29.21 -
29.22 -
29.23
29.24 (* init *)
29.25
30.1 --- a/src/Pure/Tools/invoke.ML Sat Oct 06 16:41:22 2007 +0200
30.2 +++ b/src/Pure/Tools/invoke.ML Sat Oct 06 16:50:04 2007 +0200
30.3 @@ -115,7 +115,7 @@
30.4
30.5 local structure P = OuterParse and K = OuterKeyword in
30.6
30.7 -val invokeP =
30.8 +val _ =
30.9 OuterSyntax.command "invoke"
30.10 "schematic invocation of locale expression in proof context"
30.11 (K.tag_proof K.prf_goal)
30.12 @@ -123,8 +123,6 @@
30.13 >> (fn (((name, expr), (insts, _)), fixes) =>
30.14 Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
30.15
30.16 -val _ = OuterSyntax.add_parsers [invokeP];
30.17 -
30.18 end;
30.19
30.20 end;
31.1 --- a/src/Pure/Tools/named_thms.ML Sat Oct 06 16:41:22 2007 +0200
31.2 +++ b/src/Pure/Tools/named_thms.ML Sat Oct 06 16:50:04 2007 +0200
31.3 @@ -36,10 +36,10 @@
31.4 val setup =
31.5 Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
31.6
31.7 -val _ = OuterSyntax.add_parsers
31.8 - [OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
31.9 +val _ =
31.10 + OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
31.11 OuterKeyword.diag
31.12 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
31.13 - Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)))];
31.14 + Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
31.15
31.16 end;
32.1 --- a/src/Pure/codegen.ML Sat Oct 06 16:41:22 2007 +0200
32.2 +++ b/src/Pure/codegen.ML Sat Oct 06 16:50:04 2007 +0200
32.3 @@ -1100,6 +1100,8 @@
32.4
32.5 structure P = OuterParse and K = OuterKeyword;
32.6
32.7 +val _ = OuterSyntax.keywords ["attach", "file", "contains"];
32.8 +
32.9 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
32.10 (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
32.11
32.12 @@ -1107,7 +1109,7 @@
32.13 Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
32.14 (P.verbatim >> strip_whitespace));
32.15
32.16 -val assoc_typeP =
32.17 +val _ =
32.18 OuterSyntax.command "types_code"
32.19 "associate types with target language types" K.thy_decl
32.20 (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
32.21 @@ -1115,7 +1117,7 @@
32.22 (fn ((name, mfx), aux) => (name, (parse_mixfix
32.23 (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
32.24
32.25 -val assoc_constP =
32.26 +val _ =
32.27 OuterSyntax.command "consts_code"
32.28 "associate constants with target language code" K.thy_decl
32.29 (Scan.repeat1
32.30 @@ -1152,12 +1154,12 @@
32.31 else map_modules (Symtab.update (module, gr)) thy)
32.32 end));
32.33
32.34 -val code_libraryP =
32.35 +val _ =
32.36 OuterSyntax.command "code_library"
32.37 "generates code for terms (one structure for each theory)" K.thy_decl
32.38 (parse_code true);
32.39
32.40 -val code_moduleP =
32.41 +val _ =
32.42 OuterSyntax.command "code_module"
32.43 "generates code for terms (single structure, incremental)" K.thy_decl
32.44 (parse_code false);
32.45 @@ -1174,13 +1176,13 @@
32.46 (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
32.47 fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
32.48
32.49 -val test_paramsP =
32.50 +val _ =
32.51 OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
32.52 (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
32.53 (fn fs => Toplevel.theory (fn thy =>
32.54 map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
32.55
32.56 -val testP =
32.57 +val _ =
32.58 OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
32.59 (Scan.option (P.$$$ "[" |-- P.list1
32.60 ( parse_test_params >> (fn f => fn thy => apfst (f thy))
32.61 @@ -1191,15 +1193,10 @@
32.62 (get_test_params (Toplevel.theory_of st), [])) g [] |>
32.63 pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
32.64
32.65 -val valueP =
32.66 +val _ =
32.67 OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
32.68 (P.term >> (Toplevel.no_timing oo print_evaluated_term));
32.69
32.70 -val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
32.71 -
32.72 -val _ = OuterSyntax.add_parsers
32.73 - [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
32.74 -
32.75 end;
32.76
32.77 val auto_quickcheck = Codegen.auto_quickcheck;
33.1 --- a/src/Tools/code/code_package.ML Sat Oct 06 16:41:22 2007 +0200
33.2 +++ b/src/Tools/code/code_package.ML Sat Oct 06 16:50:04 2007 +0200
33.3 @@ -558,14 +558,14 @@
33.4 -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
33.5 ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
33.6
33.7 -val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
33.8 +val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
33.9
33.10 val (codeK, code_thmsK, code_depsK, code_propsK) =
33.11 ("export_code", "code_thms", "code_deps", "code_props");
33.12
33.13 in
33.14
33.15 -val codeP =
33.16 +val _ =
33.17 OuterSyntax.improper_command codeK "generate executable code for constants"
33.18 K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
33.19
33.20 @@ -574,24 +574,22 @@
33.21 of SOME f => (writeln "Now generating code..."; f thy)
33.22 | NONE => error ("Bad directive " ^ quote cmd);
33.23
33.24 -val code_thmsP =
33.25 +val _ =
33.26 OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
33.27 (Scan.repeat P.term
33.28 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
33.29 o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
33.30
33.31 -val code_depsP =
33.32 +val _ =
33.33 OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
33.34 (Scan.repeat P.term
33.35 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
33.36 o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
33.37
33.38 -val code_propsP =
33.39 +val _ =
33.40 OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
33.41 K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
33.42
33.43 -val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP, code_propsP];
33.44 -
33.45 end; (*local*)
33.46
33.47 end; (*struct*)
34.1 --- a/src/Tools/code/code_target.ML Sat Oct 06 16:41:22 2007 +0200
34.2 +++ b/src/Tools/code/code_target.ML Sat Oct 06 16:50:04 2007 +0200
34.3 @@ -2091,7 +2091,10 @@
34.4
34.5 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
34.6
34.7 -val code_classP =
34.8 +
34.9 +val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
34.10 +
34.11 +val _ =
34.12 OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
34.13 parse_multi_syntax P.xname
34.14 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
34.15 @@ -2100,7 +2103,7 @@
34.16 fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
34.17 );
34.18
34.19 -val code_instanceP =
34.20 +val _ =
34.21 OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
34.22 parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
34.23 ((P.minus >> K true) || Scan.succeed false)
34.24 @@ -2108,55 +2111,50 @@
34.25 fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
34.26 );
34.27
34.28 -val code_typeP =
34.29 +val _ =
34.30 OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
34.31 parse_multi_syntax P.xname (parse_syntax I)
34.32 >> (Toplevel.theory oo fold) (fn (target, syns) =>
34.33 fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
34.34 );
34.35
34.36 -val code_constP =
34.37 +val _ =
34.38 OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
34.39 parse_multi_syntax P.term (parse_syntax fst)
34.40 >> (Toplevel.theory oo fold) (fn (target, syns) =>
34.41 fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
34.42 );
34.43
34.44 -val code_monadP =
34.45 +val _ =
34.46 OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
34.47 P.term -- P.term -- P.term
34.48 >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory
34.49 (add_haskell_monad raw_run raw_mbind raw_kbind))
34.50 );
34.51
34.52 -val code_reservedP =
34.53 +val _ =
34.54 OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
34.55 P.name -- Scan.repeat1 P.name
34.56 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
34.57 );
34.58
34.59 -val code_modulenameP =
34.60 +val _ =
34.61 OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
34.62 P.name -- Scan.repeat1 (P.name -- P.name)
34.63 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
34.64 );
34.65
34.66 -val code_moduleprologP =
34.67 +val _ =
34.68 OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
34.69 P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
34.70 >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
34.71 );
34.72
34.73 -val code_exceptionP =
34.74 +val _ =
34.75 OuterSyntax.command code_exceptionK "permit exceptions for constant" K.thy_decl (
34.76 Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
34.77 );
34.78
34.79 -val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
34.80 -
34.81 -val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
34.82 - code_reservedP, code_modulenameP, code_moduleprologP, code_monadP, code_exceptionP];
34.83 -
34.84
34.85 (*including serializer defaults*)
34.86 val setup =
35.1 --- a/src/Tools/induct.ML Sat Oct 06 16:41:22 2007 +0200
35.2 +++ b/src/Tools/induct.ML Sat Oct 06 16:50:04 2007 +0200
35.3 @@ -161,10 +161,10 @@
35.4 |> Pretty.chunks |> Pretty.writeln
35.5 end;
35.6
35.7 -val _ = OuterSyntax.add_parsers [
35.8 +val _ =
35.9 OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
35.10 OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
35.11 - Toplevel.keep (print_rules o Toplevel.context_of)))];
35.12 + Toplevel.keep (print_rules o Toplevel.context_of)));
35.13
35.14
35.15 (* access rules *)
36.1 --- a/src/Tools/nbe.ML Sat Oct 06 16:41:22 2007 +0200
36.2 +++ b/src/Tools/nbe.ML Sat Oct 06 16:50:04 2007 +0200
36.3 @@ -410,12 +410,10 @@
36.4
36.5 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
36.6
36.7 -val nbeP =
36.8 +val _ =
36.9 OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
36.10 (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
36.11
36.12 -val _ = OuterSyntax.add_parsers [nbeP];
36.13 -
36.14 end;
36.15
36.16 end;
37.1 --- a/src/ZF/Tools/datatype_package.ML Sat Oct 06 16:41:22 2007 +0200
37.2 +++ b/src/ZF/Tools/datatype_package.ML Sat Oct 06 16:50:04 2007 +0200
37.3 @@ -422,11 +422,9 @@
37.4
37.5 val coind_prefix = if coind then "co" else "";
37.6
37.7 -val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
37.8 +val _ = OuterSyntax.command (coind_prefix ^ "datatype")
37.9 ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
37.10
37.11 -val _ = OuterSyntax.add_parsers [inductiveP];
37.12 -
37.13 end;
37.14
37.15 end;
38.1 --- a/src/ZF/Tools/ind_cases.ML Sat Oct 06 16:41:22 2007 +0200
38.2 +++ b/src/ZF/Tools/ind_cases.ML Sat Oct 06 16:50:04 2007 +0200
38.3 @@ -76,15 +76,11 @@
38.4
38.5 local structure P = OuterParse and K = OuterKeyword in
38.6
38.7 -val ind_cases =
38.8 - P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
38.9 - >> (Toplevel.theory o inductive_cases);
38.10 -
38.11 -val inductive_casesP =
38.12 +val _ =
38.13 OuterSyntax.command "inductive_cases"
38.14 - "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
38.15 -
38.16 -val _ = OuterSyntax.add_parsers [inductive_casesP];
38.17 + "create simplified instances of elimination rules (improper)" K.thy_script
38.18 + (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
38.19 + >> (Toplevel.theory o inductive_cases));
38.20
38.21 end;
38.22
39.1 --- a/src/ZF/Tools/induct_tacs.ML Sat Oct 06 16:41:22 2007 +0200
39.2 +++ b/src/ZF/Tools/induct_tacs.ML Sat Oct 06 16:50:04 2007 +0200
39.3 @@ -188,6 +188,8 @@
39.4
39.5 local structure P = OuterParse and K = OuterKeyword in
39.6
39.7 +val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
39.8 +
39.9 val rep_datatype_decl =
39.10 (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
39.11 (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
39.12 @@ -195,13 +197,10 @@
39.13 Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
39.14 >> (fn (((x, y), z), w) => rep_datatype x y z w);
39.15
39.16 -val rep_datatypeP =
39.17 +val _ =
39.18 OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
39.19 (rep_datatype_decl >> Toplevel.theory);
39.20
39.21 -val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
39.22 -val _ = OuterSyntax.add_parsers [rep_datatypeP];
39.23 -
39.24 end;
39.25
39.26 end;
40.1 --- a/src/ZF/Tools/inductive_package.ML Sat Oct 06 16:41:22 2007 +0200
40.2 +++ b/src/ZF/Tools/inductive_package.ML Sat Oct 06 16:50:04 2007 +0200
40.3 @@ -576,6 +576,9 @@
40.4
40.5 local structure P = OuterParse and K = OuterKeyword in
40.6
40.7 +val _ = OuterSyntax.keywords
40.8 + ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
40.9 +
40.10 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
40.11 #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
40.12
40.13 @@ -590,13 +593,9 @@
40.14 Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
40.15 >> (Toplevel.theory o mk_ind);
40.16
40.17 -val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
40.18 +val _ = OuterSyntax.command (co_prefix ^ "inductive")
40.19 ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
40.20
40.21 -val _ = OuterSyntax.add_keywords
40.22 - ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
40.23 -val _ = OuterSyntax.add_parsers [inductiveP];
40.24 -
40.25 end;
40.26
40.27 end;
41.1 --- a/src/ZF/Tools/primrec_package.ML Sat Oct 06 16:41:22 2007 +0200
41.2 +++ b/src/ZF/Tools/primrec_package.ML Sat Oct 06 16:50:04 2007 +0200
41.3 @@ -203,18 +203,12 @@
41.4
41.5 (* outer syntax *)
41.6
41.7 -local structure P = OuterParse and K = OuterKeyword in
41.8 +structure P = OuterParse and K = OuterKeyword;
41.9
41.10 -val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
41.11 -
41.12 -val primrecP =
41.13 +val _ =
41.14 OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
41.15 - (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
41.16 -
41.17 -val _ = OuterSyntax.add_parsers [primrecP];
41.18 + (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
41.19 + >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
41.20
41.21 end;
41.22
41.23 -end;
41.24 -
41.25 -
42.1 --- a/src/ZF/Tools/typechk.ML Sat Oct 06 16:41:22 2007 +0200
42.2 +++ b/src/ZF/Tools/typechk.ML Sat Oct 06 16:50:04 2007 +0200
42.3 @@ -118,10 +118,10 @@
42.4 Args.del -- Args.colon >> K (I, TC_del)]
42.5 (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
42.6
42.7 -val _ = OuterSyntax.add_parsers
42.8 - [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
42.9 +val _ =
42.10 + OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
42.11 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
42.12 - Toplevel.keep (print_tcset o Toplevel.context_of)))];
42.13 + Toplevel.keep (print_tcset o Toplevel.context_of)));
42.14
42.15
42.16 (* theory setup *)