1.1 --- a/src/HOL/Tools/datatype_package.ML Tue Feb 12 20:25:58 2002 +0100
1.2 +++ b/src/HOL/Tools/datatype_package.ML Tue Feb 12 20:28:27 2002 +0100
1.3 @@ -858,12 +858,13 @@
1.4
1.5 val datatype_decl =
1.6 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
1.7 - (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment));
1.8 + (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
1.9
1.10 fun mk_datatype args =
1.11 let
1.12 val names = map (fn ((((None, _), t), _), _) => t | ((((Some t, _), _), _), _) => t) args;
1.13 - val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
1.14 + val specs = map (fn ((((_, vs), t), mx), cons) =>
1.15 + (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
1.16 in #1 o add_datatype false names specs end;
1.17
1.18 val datatypeP =
2.1 --- a/src/HOL/Tools/inductive_package.ML Tue Feb 12 20:25:58 2002 +0100
2.2 +++ b/src/HOL/Tools/inductive_package.ML Tue Feb 12 20:28:27 2002 +0100
2.3 @@ -44,10 +44,8 @@
2.4 val inductive_forall_name: string
2.5 val inductive_forall_def: thm
2.6 val rulify: thm -> thm
2.7 - val inductive_cases: (((bstring * Args.src list) * string list) * Comment.text) list
2.8 - -> theory -> theory
2.9 - val inductive_cases_i: (((bstring * theory attribute list) * term list) * Comment.text) list
2.10 - -> theory -> theory
2.11 + val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
2.12 + val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
2.13 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
2.14 ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
2.15 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
2.16 @@ -587,8 +585,8 @@
2.17 val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
2.18 val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
2.19
2.20 - val facts = args |> map (fn (((a, atts), props), comment) =>
2.21 - (((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props), comment));
2.22 + val facts = args |> map (fn ((a, atts), props) =>
2.23 + ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
2.24 in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
2.25
2.26 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
2.27 @@ -874,10 +872,10 @@
2.28 #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
2.29
2.30 fun ind_decl coind =
2.31 - (Scan.repeat1 P.term --| P.marg_comment) --
2.32 + Scan.repeat1 P.term --
2.33 (P.$$$ "intros" |--
2.34 - P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
2.35 - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) []
2.36 + P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
2.37 + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
2.38 >> (Toplevel.theory o mk_ind coind);
2.39
2.40 val inductiveP =
2.41 @@ -888,7 +886,7 @@
2.42
2.43
2.44 val ind_cases =
2.45 - P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment)
2.46 + P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
2.47 >> (Toplevel.theory o inductive_cases);
2.48
2.49 val inductive_casesP =
3.1 --- a/src/HOL/Tools/primrec_package.ML Tue Feb 12 20:25:58 2002 +0100
3.2 +++ b/src/HOL/Tools/primrec_package.ML Tue Feb 12 20:28:27 2002 +0100
3.3 @@ -291,7 +291,7 @@
3.4
3.5 val primrec_decl =
3.6 Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
3.7 - Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
3.8 + Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
3.9
3.10 val primrecP =
3.11 OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
4.1 --- a/src/HOL/Tools/recdef_package.ML Tue Feb 12 20:25:58 2002 +0100
4.2 +++ b/src/HOL/Tools/recdef_package.ML Tue Feb 12 20:28:27 2002 +0100
4.3 @@ -310,8 +310,8 @@
4.4 error ("No termination condition #" ^ string_of_int i ^
4.5 " in recdef definition of " ^ quote name);
4.6 in
4.7 - thy |> IsarThy.theorem_i Drule.internalK
4.8 - (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
4.9 + thy
4.10 + |> IsarThy.theorem_i Drule.internalK ((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))) int
4.11 end;
4.12
4.13 val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
4.14 @@ -340,8 +340,7 @@
4.15
4.16 val recdef_decl =
4.17 Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
4.18 - P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment)
4.19 - -- Scan.option hints
4.20 + P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop) -- Scan.option hints
4.21 >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
4.22
4.23 val recdefP =
4.24 @@ -360,8 +359,7 @@
4.25
4.26
4.27 val recdef_tc_decl =
4.28 - P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
4.29 - --| P.marg_comment;
4.30 + P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")");
4.31
4.32 fun mk_recdef_tc ((thm_name, name), i) = recdef_tc thm_name name i;
4.33
5.1 --- a/src/HOL/Tools/record_package.ML Tue Feb 12 20:25:58 2002 +0100
5.2 +++ b/src/HOL/Tools/record_package.ML Tue Feb 12 20:28:27 2002 +0100
5.3 @@ -1086,8 +1086,8 @@
5.4 local structure P = OuterParse and K = OuterSyntax.Keyword in
5.5
5.6 val record_decl =
5.7 - P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+")
5.8 - -- Scan.repeat1 (P.const --| P.marg_comment));
5.9 + P.type_args -- P.name --
5.10 + (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
5.11
5.12 val recordP =
5.13 OuterSyntax.command "record" "define extensible record" K.thy_decl
6.1 --- a/src/HOL/Tools/typedef_package.ML Tue Feb 12 20:25:58 2002 +0100
6.2 +++ b/src/HOL/Tools/typedef_package.ML Tue Feb 12 20:28:27 2002 +0100
6.3 @@ -22,11 +22,9 @@
6.4 {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
6.5 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
6.6 Rep_induct: thm, Abs_induct: thm}
6.7 - val typedef_proof:
6.8 - (string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text
6.9 + val typedef_proof: string * (bstring * string list * mixfix) * string * (string * string) option
6.10 -> bool -> theory -> ProofHistory.T
6.11 - val typedef_proof_i:
6.12 - (string * (bstring * string list * mixfix) * term * (string * string) option) * Comment.text
6.13 + val typedef_proof_i: string * (bstring * string list * mixfix) * term * (string * string) option
6.14 -> bool -> theory -> ProofHistory.T
6.15 end;
6.16
6.17 @@ -241,15 +239,12 @@
6.18
6.19 (* typedef_proof interface *)
6.20
6.21 -fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy =
6.22 +fun gen_typedef_proof prep_term (name, typ, set, opt_morphs) int thy =
6.23 let
6.24 val (_, goal, goal_pat, att_result) =
6.25 prepare_typedef prep_term true name typ set opt_morphs thy;
6.26 val att = #1 o att_result;
6.27 - in
6.28 - thy
6.29 - |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
6.30 - end;
6.31 + in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end;
6.32
6.33 val typedef_proof = gen_typedef_proof read_term;
6.34 val typedef_proof_i = gen_typedef_proof cert_term;
6.35 @@ -262,18 +257,17 @@
6.36
6.37 val typedeclP =
6.38 OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
6.39 - (P.type_args -- P.name -- P.opt_infix --| P.marg_comment >> (fn ((vs, t), mx) =>
6.40 + (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
6.41 Toplevel.theory (add_typedecls [(t, vs, mx)])));
6.42
6.43
6.44 val typedef_proof_decl =
6.45 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
6.46 (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
6.47 - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)) --
6.48 - P.marg_comment;
6.49 + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
6.50
6.51 -fun mk_typedef_proof (((((opt_name, (vs, t)), mx), A), morphs), comment) =
6.52 - typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs), comment);
6.53 +fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), morphs) =
6.54 + typedef_proof (if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs);
6.55
6.56 val typedefP =
6.57 OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
6.58 @@ -285,5 +279,4 @@
6.59
6.60 end;
6.61
6.62 -
6.63 end;
7.1 --- a/src/HOLCF/cont_consts.ML Tue Feb 12 20:25:58 2002 +0100
7.2 +++ b/src/HOLCF/cont_consts.ML Tue Feb 12 20:28:27 2002 +0100
7.3 @@ -110,7 +110,7 @@
7.4 thy
7.5 |> consts (map fst args)
7.6 |> defs (false, map (fn ((c, _, mx), s) =>
7.7 - (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
7.8 + ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
7.9
7.10 fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args;
7.11 fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args;
7.12 @@ -122,12 +122,11 @@
7.13
7.14 val constsP =
7.15 OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
7.16 - (Scan.repeat1 (P.const --| P.marg_comment) >> (Toplevel.theory o add_consts));
7.17 + (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
7.18
7.19 val constdefsP =
7.20 OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl
7.21 - (Scan.repeat1 ((P.const --| P.marg_comment) -- (P.term --| P.marg_comment))
7.22 - >> (Toplevel.theory o add_constdefs));
7.23 + (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs));
7.24
7.25
7.26 val _ = OuterSyntax.add_parsers [constsP, constdefsP];
8.1 --- a/src/HOLCF/domain/extender.ML Tue Feb 12 20:25:58 2002 +0100
8.2 +++ b/src/HOLCF/domain/extender.ML Tue Feb 12 20:28:27 2002 +0100
8.3 @@ -124,7 +124,7 @@
8.4 P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1;
8.5
8.6 val cons_decl =
8.7 - P.name -- Scan.repeat dest_decl -- P.opt_mixfix --| P.marg_comment
8.8 + P.name -- Scan.repeat dest_decl -- P.opt_mixfix
8.9 >> (fn ((c, ds), mx) => (c, mx, ds));
8.10
8.11 val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
9.1 --- a/src/Pure/Isar/isar_cmd.ML Tue Feb 12 20:25:58 2002 +0100
9.2 +++ b/src/Pure/Isar/isar_cmd.ML Tue Feb 12 20:28:27 2002 +0100
9.3 @@ -29,11 +29,10 @@
9.4 val undo_theory: Toplevel.transition -> Toplevel.transition
9.5 val undo: Toplevel.transition -> Toplevel.transition
9.6 val kill: Toplevel.transition -> Toplevel.transition
9.7 - val back: bool * Comment.text -> Toplevel.transition -> Toplevel.transition
9.8 - val use: string * Comment.text -> Toplevel.transition -> Toplevel.transition
9.9 - val use_mltext_theory: string * Comment.text -> Toplevel.transition -> Toplevel.transition
9.10 - val use_mltext: bool -> string * Comment.text -> Toplevel.transition -> Toplevel.transition
9.11 - val use_setup: string * Comment.text -> theory -> theory
9.12 + val back: bool -> Toplevel.transition -> Toplevel.transition
9.13 + val use: string -> Toplevel.transition -> Toplevel.transition
9.14 + val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
9.15 + val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
9.16 val use_commit: Toplevel.transition -> Toplevel.transition
9.17 val cd: string -> Toplevel.transition -> Toplevel.transition
9.18 val pwd: Toplevel.transition -> Toplevel.transition
9.19 @@ -47,7 +46,7 @@
9.20 val print_syntax: Toplevel.transition -> Toplevel.transition
9.21 val print_theorems: Toplevel.transition -> Toplevel.transition
9.22 val print_locales: Toplevel.transition -> Toplevel.transition
9.23 - val print_locale: Locale.expr * (Args.src Locale.element * Comment.text) list
9.24 + val print_locale: Locale.expr * Args.src Locale.element list
9.25 -> Toplevel.transition -> Toplevel.transition
9.26 val print_attributes: Toplevel.transition -> Toplevel.transition
9.27 val print_rules: Toplevel.transition -> Toplevel.transition
9.28 @@ -60,16 +59,13 @@
9.29 val print_binds: Toplevel.transition -> Toplevel.transition
9.30 val print_lthms: Toplevel.transition -> Toplevel.transition
9.31 val print_cases: Toplevel.transition -> Toplevel.transition
9.32 - val print_thms: (string list * (string * Args.src list) list) * Comment.text
9.33 + val print_thms: string list * (string * Args.src list) list
9.34 -> Toplevel.transition -> Toplevel.transition
9.35 - val print_prfs: bool -> (string list * (string * Args.src list) list option) * Comment.text
9.36 + val print_prfs: bool -> string list * (string * Args.src list) list option
9.37 -> Toplevel.transition -> Toplevel.transition
9.38 - val print_prop: (string list * string) * Comment.text
9.39 - -> Toplevel.transition -> Toplevel.transition
9.40 - val print_term: (string list * string) * Comment.text
9.41 - -> Toplevel.transition -> Toplevel.transition
9.42 - val print_type: (string list * string) * Comment.text
9.43 - -> Toplevel.transition -> Toplevel.transition
9.44 + val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
9.45 + val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
9.46 + val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
9.47 end;
9.48
9.49 structure IsarCmd: ISAR_CMD =
9.50 @@ -135,26 +131,23 @@
9.51
9.52 val undo = Toplevel.kill o undo_theory o undos_proof 1;
9.53 val kill = Toplevel.kill o kill_proof;
9.54 -
9.55 -val back = Toplevel.proof o ProofHistory.back o Comment.ignore;
9.56 +val back = Toplevel.proof o ProofHistory.back;
9.57
9.58
9.59 (* use ML text *)
9.60
9.61 -fun use (name, comment_ignore) = Toplevel.keep (fn state =>
9.62 +fun use name = Toplevel.keep (fn state =>
9.63 Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
9.64
9.65 (*passes changes of theory context*)
9.66 -val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore;
9.67 +val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
9.68
9.69 (*ignore result theory context*)
9.70 -fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state =>
9.71 +fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
9.72 (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
9.73
9.74 -val use_setup = Context.use_setup o Comment.ignore;
9.75 -
9.76 (*Note: commit is dynamically bound*)
9.77 -val use_commit = use_mltext false ("commit();", Comment.none);
9.78 +val use_commit = use_mltext false "commit();";
9.79
9.80
9.81 (* current working directory *)
9.82 @@ -196,8 +189,7 @@
9.83
9.84 fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
9.85 let val thy = Toplevel.theory_of state in
9.86 - Locale.print_locale thy import
9.87 - (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body)
9.88 + Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body)
9.89 end);
9.90
9.91 val print_attributes = Toplevel.unknown_theory o
9.92 @@ -291,11 +283,10 @@
9.93 fun print_item string_of (x, y) = Toplevel.keep (fn state =>
9.94 writeln (string_of (Toplevel.enter_forward_proof state) x y));
9.95
9.96 -val print_thms = print_item string_of_thms o Comment.ignore;
9.97 -fun print_prfs full = print_item (string_of_prfs full) o Comment.ignore;
9.98 -val print_prop = print_item string_of_prop o Comment.ignore;
9.99 -val print_term = print_item string_of_term o Comment.ignore;
9.100 -val print_type = print_item string_of_type o Comment.ignore;
9.101 -
9.102 +val print_thms = print_item string_of_thms;
9.103 +fun print_prfs full = print_item (string_of_prfs full);
9.104 +val print_prop = print_item string_of_prop;
9.105 +val print_term = print_item string_of_term;
9.106 +val print_type = print_item string_of_type;
9.107
9.108 end;
10.1 --- a/src/Pure/Isar/isar_syn.ML Tue Feb 12 20:25:58 2002 +0100
10.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Feb 12 20:28:27 2002 +0100
10.3 @@ -37,45 +37,45 @@
10.4 (** markup commands **)
10.5
10.6 val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag
10.7 - (P.comment >> IsarThy.add_header);
10.8 + (P.text >> IsarThy.add_header);
10.9
10.10 val chapterP = OuterSyntax.markup_command IsarOutput.Markup "chapter" "chapter heading"
10.11 - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
10.12 + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_chapter));
10.13
10.14 val sectionP = OuterSyntax.markup_command IsarOutput.Markup "section" "section heading"
10.15 - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_section));
10.16 + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_section));
10.17
10.18 val subsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsection" "subsection heading"
10.19 - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
10.20 + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_subsection));
10.21
10.22 val subsubsectionP =
10.23 OuterSyntax.markup_command IsarOutput.Markup "subsubsection" "subsubsection heading"
10.24 - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
10.25 + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_subsubsection));
10.26
10.27 val textP = OuterSyntax.markup_command IsarOutput.MarkupEnv "text" "formal comment (theory)"
10.28 - K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text));
10.29 + K.thy_decl (P.text >> (Toplevel.theory o IsarThy.add_text));
10.30
10.31 val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw"
10.32 "raw document preparation text" K.thy_decl
10.33 - (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
10.34 + (P.text >> (Toplevel.theory o IsarThy.add_text_raw));
10.35
10.36
10.37 val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
10.38 - K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
10.39 + K.prf_heading (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
10.40
10.41 val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
10.42 - K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
10.43 + K.prf_heading (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
10.44
10.45 val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
10.46 "formal comment (proof)" K.prf_heading
10.47 - (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
10.48 + (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
10.49
10.50 val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
10.51 - K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
10.52 + K.prf_decl (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
10.53
10.54 val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw"
10.55 "raw document preparation text (proof)" K.prf_decl
10.56 - (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
10.57 + (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
10.58
10.59
10.60
10.61 @@ -86,53 +86,51 @@
10.62 val classesP =
10.63 OuterSyntax.command "classes" "declare type classes" K.thy_decl
10.64 (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
10.65 - P.!!! (P.list1 P.xname)) [])
10.66 - -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
10.67 + P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o Theory.add_classes));
10.68
10.69 val classrelP =
10.70 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
10.71 - (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) -- P.marg_comment
10.72 - >> (Toplevel.theory o IsarThy.add_classrel));
10.73 + (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
10.74 + >> (Toplevel.theory o Theory.add_classrel o single));
10.75
10.76 val defaultsortP =
10.77 OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
10.78 - (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));
10.79 + (P.sort >> (Toplevel.theory o Theory.add_defsort));
10.80
10.81
10.82 (* types *)
10.83
10.84 val typedeclP =
10.85 OuterSyntax.command "typedecl" "type declaration" K.thy_decl
10.86 - (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
10.87 - Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
10.88 + (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
10.89 + Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
10.90
10.91 val typeabbrP =
10.92 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
10.93 (Scan.repeat1
10.94 - (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment)
10.95 - >> (Toplevel.theory o IsarThy.add_tyabbrs o
10.96 - map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
10.97 + (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
10.98 + >> (Toplevel.theory o Theory.add_tyabbrs o
10.99 + map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
10.100
10.101 val nontermP =
10.102 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
10.103 - K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment)
10.104 - >> (Toplevel.theory o IsarThy.add_nonterminals));
10.105 + K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
10.106
10.107 val aritiesP =
10.108 OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
10.109 - (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment)
10.110 - >> (Toplevel.theory o IsarThy.add_arities));
10.111 + (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
10.112 + >> (Toplevel.theory o Theory.add_arities));
10.113
10.114
10.115 (* consts and syntax *)
10.116
10.117 val judgmentP =
10.118 OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
10.119 - (P.const -- P.marg_comment >> (Toplevel.theory o IsarThy.add_judgment));
10.120 + (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
10.121
10.122 val constsP =
10.123 OuterSyntax.command "consts" "declare constants" K.thy_decl
10.124 - (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
10.125 + (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
10.126
10.127
10.128 val mode_spec =
10.129 @@ -142,8 +140,7 @@
10.130
10.131 val syntaxP =
10.132 OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
10.133 - (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment)
10.134 - >> (Toplevel.theory o uncurry IsarThy.add_modesyntax));
10.135 + (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
10.136
10.137
10.138 (* translations *)
10.139 @@ -162,33 +159,31 @@
10.140
10.141 val translationsP =
10.142 OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
10.143 - (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules));
10.144 + (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
10.145
10.146
10.147 (* axioms and definitions *)
10.148
10.149 val axiomsP =
10.150 OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
10.151 - (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
10.152 + (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
10.153
10.154 val opt_overloaded =
10.155 Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
10.156
10.157 val defsP =
10.158 OuterSyntax.command "defs" "define constants" K.thy_decl
10.159 - (opt_overloaded -- Scan.repeat1 (P.spec_name -- P.marg_comment)
10.160 - >> (Toplevel.theory o IsarThy.add_defs));
10.161 + (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
10.162
10.163 val constdefsP =
10.164 OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
10.165 - (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment))
10.166 - >> (Toplevel.theory o IsarThy.add_constdefs));
10.167 + (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o IsarThy.add_constdefs));
10.168
10.169
10.170 (* theorems *)
10.171
10.172 val in_locale = Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname --| P.$$$ ")"));
10.173 -val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1 -- P.marg_comment);
10.174 +val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1);
10.175
10.176 fun theorems kind = in_locale -- name_facts
10.177 >> uncurry (#1 ooo IsarThy.smart_theorems kind);
10.178 @@ -203,93 +198,92 @@
10.179
10.180 val declareP =
10.181 OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
10.182 - (in_locale -- (P.xthms1 -- P.marg_comment)
10.183 - >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
10.184 + (in_locale -- P.xthms1 >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
10.185
10.186
10.187 (* name space entry path *)
10.188
10.189 val globalP =
10.190 OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
10.191 - (P.marg_comment >> (Toplevel.theory o IsarThy.global_path));
10.192 + (Scan.succeed (Toplevel.theory PureThy.global_path));
10.193
10.194 val localP =
10.195 OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
10.196 - (P.marg_comment >> (Toplevel.theory o IsarThy.local_path));
10.197 + (Scan.succeed (Toplevel.theory PureThy.local_path));
10.198
10.199 val hideP =
10.200 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
10.201 - (P.name -- Scan.repeat1 P.xname -- P.marg_comment >> (Toplevel.theory o IsarThy.hide_space));
10.202 + (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_space));
10.203
10.204
10.205 (* use ML text *)
10.206
10.207 val useP =
10.208 OuterSyntax.command "use" "eval ML text from file" K.diag
10.209 - (P.name -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use));
10.210 + (P.name >> (Toplevel.no_timing oo IsarCmd.use));
10.211
10.212 val mlP =
10.213 OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
10.214 - (P.text -- P.marg_comment >> IsarCmd.use_mltext true);
10.215 + (P.text >> IsarCmd.use_mltext true);
10.216
10.217 val ml_commandP =
10.218 OuterSyntax.command "ML_command" "eval ML text" K.diag
10.219 - (P.text -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
10.220 + (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
10.221
10.222 val ml_setupP =
10.223 OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
10.224 - (P.text -- P.marg_comment >> IsarCmd.use_mltext_theory);
10.225 + (P.text >> IsarCmd.use_mltext_theory);
10.226
10.227 val setupP =
10.228 OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
10.229 - (P.text -- P.marg_comment >> (Toplevel.theory o IsarCmd.use_setup));
10.230 + (P.text >> (Toplevel.theory o Context.use_setup));
10.231
10.232 val method_setupP =
10.233 OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
10.234 - (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2)
10.235 - -- P.marg_comment) >> (Toplevel.theory o IsarThy.method_setup));
10.236 + (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
10.237 + >> (Toplevel.theory o IsarThy.method_setup));
10.238
10.239
10.240 (* translation functions *)
10.241
10.242 val parse_ast_translationP =
10.243 OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
10.244 - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_ast_translation));
10.245 + (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
10.246
10.247 val parse_translationP =
10.248 OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
10.249 - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_translation));
10.250 + (P.text >> (Toplevel.theory o IsarThy.parse_translation));
10.251
10.252 val print_translationP =
10.253 OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
10.254 - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_translation));
10.255 + (P.text >> (Toplevel.theory o IsarThy.print_translation));
10.256
10.257 val typed_print_translationP =
10.258 OuterSyntax.command "typed_print_translation" "install typed print translation functions"
10.259 - K.thy_decl (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.typed_print_translation));
10.260 + K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
10.261
10.262 val print_ast_translationP =
10.263 OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
10.264 - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_ast_translation));
10.265 + (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
10.266
10.267 val token_translationP =
10.268 OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
10.269 - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.token_translation));
10.270 + (P.text >> (Toplevel.theory o IsarThy.token_translation));
10.271
10.272
10.273 (* oracles *)
10.274
10.275 val oracleP =
10.276 OuterSyntax.command "oracle" "install oracle" K.thy_decl
10.277 - ((P.name --| P.$$$ "=") -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle));
10.278 + ((P.name --| P.$$$ "=") -- P.text >> (Toplevel.theory o IsarThy.add_oracle));
10.279
10.280
10.281 (* locales *)
10.282
10.283 val locale_val =
10.284 (P.locale_expr --
10.285 - Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] ||
10.286 - Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty);
10.287 + Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.locale_element)) [] ||
10.288 + Scan.repeat1 P.locale_element >> pair Locale.empty);
10.289
10.290 val localeP =
10.291 OuterSyntax.command "locale" "define named proof context" K.thy_decl
10.292 @@ -305,7 +299,7 @@
10.293 val in_locale_elems = in_locale --
10.294 Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) [];
10.295
10.296 -val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
10.297 +val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
10.298 val statement' = P.$$$ "(" |-- statement --| P.!!! (P.$$$ ")") || statement;
10.299
10.300 fun gen_theorem k =
10.301 @@ -337,11 +331,11 @@
10.302
10.303 (* facts *)
10.304
10.305 -val facts = P.and_list1 (P.xthms1 -- P.marg_comment);
10.306 +val facts = P.and_list1 P.xthms1;
10.307
10.308 val thenP =
10.309 OuterSyntax.command "then" "forward chaining" K.prf_chain
10.310 - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
10.311 + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.chain)));
10.312
10.313 val fromP =
10.314 OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
10.315 @@ -360,7 +354,7 @@
10.316
10.317 val fixP =
10.318 OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
10.319 - (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
10.320 + (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
10.321 >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
10.322
10.323 val assumeP =
10.324 @@ -374,19 +368,19 @@
10.325 val defP =
10.326 OuterSyntax.command "def" "local definition" K.prf_asm
10.327 (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))
10.328 - -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
10.329 + >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
10.330
10.331 val obtainP =
10.332 OuterSyntax.command "obtain" "generalized existence"
10.333 K.prf_asm_goal
10.334 (Scan.optional
10.335 - (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
10.336 + (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
10.337 --| P.$$$ "where") [] -- statement
10.338 >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
10.339
10.340 val letP =
10.341 OuterSyntax.command "let" "bind text variables" K.prf_decl
10.342 - (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
10.343 + (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
10.344 >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
10.345
10.346 val case_spec =
10.347 @@ -395,109 +389,105 @@
10.348
10.349 val caseP =
10.350 OuterSyntax.command "case" "invoke local context" K.prf_asm
10.351 - (case_spec -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
10.352 + (case_spec >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
10.353
10.354
10.355 (* proof structure *)
10.356
10.357 val beginP =
10.358 OuterSyntax.command "{" "begin explicit proof block" K.prf_open
10.359 - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block)));
10.360 + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.begin_block)));
10.361
10.362 val endP =
10.363 OuterSyntax.command "}" "end explicit proof block" K.prf_close
10.364 - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block)));
10.365 + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.end_block)));
10.366
10.367 val nextP =
10.368 OuterSyntax.command "next" "enter next proof block" K.prf_block
10.369 - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.next_block)));
10.370 + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.next_block)));
10.371
10.372
10.373 (* end proof *)
10.374
10.375 val qedP =
10.376 OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
10.377 - (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed);
10.378 + (Scan.option P.method >> IsarThy.qed);
10.379
10.380 val terminal_proofP =
10.381 OuterSyntax.command "by" "terminal backward proof" K.qed
10.382 - (P.method -- P.interest -- Scan.option (P.method -- P.interest)
10.383 - -- P.marg_comment >> IsarThy.terminal_proof);
10.384 + (P.method -- Scan.option P.method >> IsarThy.terminal_proof);
10.385
10.386 val default_proofP =
10.387 OuterSyntax.command ".." "default proof" K.qed
10.388 - (P.marg_comment >> IsarThy.default_proof);
10.389 + (Scan.succeed IsarThy.default_proof);
10.390
10.391 val immediate_proofP =
10.392 OuterSyntax.command "." "immediate proof" K.qed
10.393 - (P.marg_comment >> IsarThy.immediate_proof);
10.394 + (Scan.succeed IsarThy.immediate_proof);
10.395
10.396 val done_proofP =
10.397 OuterSyntax.command "done" "done proof" K.qed
10.398 - (P.marg_comment >> IsarThy.done_proof);
10.399 + (Scan.succeed IsarThy.done_proof);
10.400
10.401 val skip_proofP =
10.402 OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
10.403 - (P.marg_comment >> IsarThy.skip_proof);
10.404 + (Scan.succeed IsarThy.skip_proof);
10.405
10.406 val forget_proofP =
10.407 OuterSyntax.command "oops" "forget proof" K.qed_global
10.408 - (P.marg_comment >> IsarThy.forget_proof);
10.409 -
10.410 + (Scan.succeed IsarThy.forget_proof);
10.411
10.412
10.413 (* proof steps *)
10.414
10.415 val deferP =
10.416 OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script
10.417 - (Scan.option P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
10.418 + (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
10.419
10.420 val preferP =
10.421 OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script
10.422 - (P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
10.423 + (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
10.424
10.425 val applyP =
10.426 OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script
10.427 - (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
10.428 + (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
10.429
10.430 val apply_endP =
10.431 OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script
10.432 - (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
10.433 + (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
10.434
10.435 val proofP =
10.436 OuterSyntax.command "proof" "backward proof" K.prf_block
10.437 - (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
10.438 - >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
10.439 + (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
10.440
10.441
10.442 (* calculational proof commands *)
10.443
10.444 val calc_args =
10.445 - Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
10.446 + Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")")));
10.447
10.448 val alsoP =
10.449 OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl
10.450 - (calc_args -- P.marg_comment >> IsarThy.also);
10.451 + (calc_args >> IsarThy.also);
10.452
10.453 val finallyP =
10.454 OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain
10.455 - (calc_args -- P.marg_comment >> IsarThy.finally);
10.456 + (calc_args >> IsarThy.finally);
10.457
10.458 val moreoverP =
10.459 OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
10.460 - (P.marg_comment >> IsarThy.moreover);
10.461 + (Scan.succeed IsarThy.moreover);
10.462
10.463 val ultimatelyP =
10.464 OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
10.465 - K.prf_chain (P.marg_comment >> IsarThy.ultimately);
10.466 + K.prf_chain (Scan.succeed IsarThy.ultimately);
10.467
10.468
10.469 (* proof navigation *)
10.470
10.471 val backP =
10.472 OuterSyntax.command "back" "backtracking of proof command" K.prf_script
10.473 - (Scan.optional (P.$$$ "!" >> K true) false -- P.marg_comment >>
10.474 - (Toplevel.print oo IsarCmd.back));
10.475 + (Scan.optional (P.$$$ "!" >> K true) false >> (Toplevel.print oo IsarCmd.back));
10.476
10.477
10.478 (* history *)
10.479 @@ -611,29 +601,27 @@
10.480
10.481 val print_thmsP =
10.482 OuterSyntax.improper_command "thm" "print theorems" K.diag
10.483 - (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_thms));
10.484 + (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
10.485
10.486 val print_prfsP =
10.487 OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
10.488 - (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >>
10.489 - (Toplevel.no_timing oo IsarCmd.print_prfs false));
10.490 + (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
10.491
10.492 val print_full_prfsP =
10.493 OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
10.494 - (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >>
10.495 - (Toplevel.no_timing oo IsarCmd.print_prfs true));
10.496 + (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
10.497
10.498 val print_propP =
10.499 OuterSyntax.improper_command "prop" "read and print proposition" K.diag
10.500 - (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prop));
10.501 + (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
10.502
10.503 val print_termP =
10.504 OuterSyntax.improper_command "term" "read and print term" K.diag
10.505 - (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_term));
10.506 + (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
10.507
10.508 val print_typeP =
10.509 OuterSyntax.improper_command "typ" "read and print type" K.diag
10.510 - (opt_modes -- P.typ -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_type));
10.511 + (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
10.512
10.513
10.514
11.1 --- a/src/Pure/Isar/isar_thy.ML Tue Feb 12 20:25:58 2002 +0100
11.2 +++ b/src/Pure/Isar/isar_thy.ML Tue Feb 12 20:28:27 2002 +0100
11.3 @@ -8,206 +8,154 @@
11.4
11.5 signature ISAR_THY =
11.6 sig
11.7 - val add_header: Comment.text -> Toplevel.transition -> Toplevel.transition
11.8 - val add_chapter: Comment.text -> theory -> theory
11.9 - val add_section: Comment.text -> theory -> theory
11.10 - val add_subsection: Comment.text -> theory -> theory
11.11 - val add_subsubsection: Comment.text -> theory -> theory
11.12 - val add_text: Comment.text -> theory -> theory
11.13 - val add_text_raw: Comment.text -> theory -> theory
11.14 - val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
11.15 - val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
11.16 - val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
11.17 - val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
11.18 - val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T
11.19 - val global_path: Comment.text -> theory -> theory
11.20 - val local_path: Comment.text -> theory -> theory
11.21 - val hide_space: (string * xstring list) * Comment.text -> theory -> theory
11.22 - val hide_space_i: (string * string list) * Comment.text -> theory -> theory
11.23 - val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
11.24 - val add_classes_i: (bclass * class list) list * Comment.text -> theory -> theory
11.25 - val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
11.26 - val add_classrel_i: (class * class) * Comment.text -> theory -> theory
11.27 - val add_defsort: string * Comment.text -> theory -> theory
11.28 - val add_defsort_i: sort * Comment.text -> theory -> theory
11.29 - val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
11.30 - val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
11.31 - -> theory -> theory
11.32 - val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
11.33 - -> theory -> theory
11.34 - val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory
11.35 - val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
11.36 - val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
11.37 - val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
11.38 - val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list -> theory -> theory
11.39 - val add_modesyntax: string * bool -> ((bstring * string * mixfix) * Comment.text) list
11.40 - -> theory -> theory
11.41 - val add_modesyntax_i: string * bool -> ((bstring * typ * mixfix) * Comment.text) list
11.42 - -> theory -> theory
11.43 - val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory
11.44 - val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory
11.45 - val add_judgment: (bstring * string * mixfix) * Comment.text -> theory -> theory
11.46 - val add_judgment_i: (bstring * typ * mixfix) * Comment.text -> theory -> theory
11.47 - val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
11.48 - val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
11.49 - -> theory -> theory
11.50 - val add_defs: bool * (((bstring * string) * Args.src list) * Comment.text) list
11.51 - -> theory -> theory
11.52 - val add_defs_i: bool * (((bstring * term) * theory attribute list) * Comment.text) list
11.53 - -> theory -> theory
11.54 - val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list
11.55 - -> theory -> theory
11.56 - val add_constdefs_i: (((bstring * typ * mixfix) * Comment.text) * (term * Comment.text)) list
11.57 - -> theory -> theory
11.58 - val theorems: string ->
11.59 - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
11.60 + val add_header: string -> Toplevel.transition -> Toplevel.transition
11.61 + val add_chapter: string -> theory -> theory
11.62 + val add_section: string -> theory -> theory
11.63 + val add_subsection: string -> theory -> theory
11.64 + val add_subsubsection: string -> theory -> theory
11.65 + val add_text: string -> theory -> theory
11.66 + val add_text_raw: string -> theory -> theory
11.67 + val add_sect: string -> ProofHistory.T -> ProofHistory.T
11.68 + val add_subsect: string -> ProofHistory.T -> ProofHistory.T
11.69 + val add_subsubsect: string -> ProofHistory.T -> ProofHistory.T
11.70 + val add_txt: string -> ProofHistory.T -> ProofHistory.T
11.71 + val add_txt_raw: string -> ProofHistory.T -> ProofHistory.T
11.72 + val hide_space: string * xstring list -> theory -> theory
11.73 + val hide_space_i: string * string list -> theory -> theory
11.74 + val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
11.75 + val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
11.76 + val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory
11.77 + val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
11.78 + val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
11.79 + val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
11.80 + val theorems: string -> ((bstring * Args.src list) * (xstring * Args.src list) list) list
11.81 -> theory -> theory * (string * thm list) list
11.82 val theorems_i: string ->
11.83 - (((bstring * theory attribute list)
11.84 - * (thm list * theory attribute list) list) * Comment.text) list
11.85 + ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
11.86 -> theory -> theory * (string * thm list) list
11.87 val locale_theorems: string -> xstring ->
11.88 - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
11.89 + ((bstring * Args.src list) * (xstring * Args.src list) list) list
11.90 -> theory -> theory * (bstring * thm list) list
11.91 val locale_theorems_i: string -> string ->
11.92 - (((bstring * Proof.context attribute list)
11.93 - * (thm list * Proof.context attribute list) list) * Comment.text) list
11.94 + ((bstring * Proof.context attribute list)
11.95 + * (thm list * Proof.context attribute list) list) list
11.96 -> theory -> theory * (string * thm list) list
11.97 val smart_theorems: string -> xstring option ->
11.98 - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
11.99 + ((bstring * Args.src list) * (xstring * Args.src list) list) list
11.100 -> theory -> theory * (string * thm list) list
11.101 - val declare_theorems: xstring option -> (xstring * Args.src list) list * Comment.text
11.102 - -> theory -> theory
11.103 + val declare_theorems: xstring option -> (xstring * Args.src list) list -> theory -> theory
11.104 val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
11.105 val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
11.106 - val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list
11.107 + val have_facts: ((string * Args.src list) * (string * Args.src list) list) list
11.108 -> ProofHistory.T -> ProofHistory.T
11.109 - val have_facts_i: (((string * Proof.context attribute list) *
11.110 - (thm * Proof.context attribute list) list) * Comment.text) list
11.111 + val have_facts_i: ((string * Proof.context attribute list) *
11.112 + (thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T
11.113 + val from_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
11.114 + val from_facts_i: (thm * Proof.context attribute list) list list
11.115 -> ProofHistory.T -> ProofHistory.T
11.116 - val from_facts: ((string * Args.src list) list * Comment.text) list
11.117 + val with_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
11.118 + val with_facts_i: (thm * Proof.context attribute list) list list
11.119 -> ProofHistory.T -> ProofHistory.T
11.120 - val from_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list
11.121 + val chain: ProofHistory.T -> ProofHistory.T
11.122 + val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
11.123 + val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
11.124 + val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
11.125 + val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
11.126 + val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T
11.127 + val invoke_case_i: string * string option list * Proof.context attribute list
11.128 -> ProofHistory.T -> ProofHistory.T
11.129 - val with_facts: ((string * Args.src list) list * Comment.text) list
11.130 - -> ProofHistory.T -> ProofHistory.T
11.131 - val with_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list
11.132 - -> ProofHistory.T -> ProofHistory.T
11.133 - val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
11.134 - val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.135 - val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.136 - val let_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.137 - val let_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.138 - val invoke_case: (string * string option list * Args.src list) * Comment.text
11.139 - -> ProofHistory.T -> ProofHistory.T
11.140 - val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text
11.141 - -> ProofHistory.T -> ProofHistory.T
11.142 - val theorem: string
11.143 - -> ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text
11.144 + val theorem: string -> (bstring * Args.src list) * (string * (string list * string list))
11.145 -> bool -> theory -> ProofHistory.T
11.146 - val theorem_i: string -> ((bstring * theory attribute list) *
11.147 - (term * (term list * term list))) * Comment.text -> bool -> theory -> ProofHistory.T
11.148 + val theorem_i: string -> (bstring * theory attribute list) *
11.149 + (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
11.150 val multi_theorem: string -> bstring * Args.src list ->
11.151 Args.src Locale.element list ->
11.152 - (((bstring * Args.src list) * (string * (string list * string list)) list)
11.153 - * Comment.text) list -> bool -> theory -> ProofHistory.T
11.154 + ((bstring * Args.src list) * (string * (string list * string list)) list) list
11.155 + -> bool -> theory -> ProofHistory.T
11.156 val multi_theorem_i: string -> bstring * theory attribute list ->
11.157 Proof.context attribute Locale.element_i list ->
11.158 - (((bstring * theory attribute list) * (term * (term list * term list)) list)
11.159 - * Comment.text) list -> bool -> theory -> ProofHistory.T
11.160 + ((bstring * theory attribute list) * (term * (term list * term list)) list) list
11.161 + -> bool -> theory -> ProofHistory.T
11.162 val locale_multi_theorem: string -> bstring * Args.src list ->
11.163 xstring -> Args.src Locale.element list ->
11.164 - (((bstring * Args.src list) * (string * (string list * string list)) list)
11.165 - * Comment.text) list -> bool -> theory -> ProofHistory.T
11.166 + ((bstring * Args.src list) * (string * (string list * string list)) list) list
11.167 + -> bool -> theory -> ProofHistory.T
11.168 val locale_multi_theorem_i: string -> bstring * theory attribute list ->
11.169 string -> Proof.context attribute Locale.element_i list ->
11.170 - (((bstring * Proof.context attribute list) * (term * (term list * term list)) list)
11.171 - * Comment.text) list -> bool -> theory -> ProofHistory.T
11.172 + ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
11.173 + -> bool -> theory -> ProofHistory.T
11.174 val smart_multi_theorem: string -> bstring * Args.src list ->
11.175 xstring Library.option * Args.src Locale.element list ->
11.176 - (((bstring * Args.src list) * (string * (string list * string list)) list)
11.177 - * Comment.text) list -> bool -> theory -> ProofHistory.T
11.178 - val assume: (((string * Args.src list) * (string * (string list * string list)) list)
11.179 - * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.180 - val assume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list)
11.181 - * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.182 - val presume: (((string * Args.src list) * (string * (string list * string list)) list)
11.183 - * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.184 - val presume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list)
11.185 - * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.186 - val have: (((string * Args.src list) *
11.187 - (string * (string list * string list)) list) * Comment.text) list
11.188 + ((bstring * Args.src list) * (string * (string list * string list)) list) list
11.189 + -> bool -> theory -> ProofHistory.T
11.190 + val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
11.191 -> ProofHistory.T -> ProofHistory.T
11.192 - val have_i: (((string * Proof.context attribute list) *
11.193 - (term * (term list * term list)) list) * Comment.text) list
11.194 + val assume_i:
11.195 + ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
11.196 -> ProofHistory.T -> ProofHistory.T
11.197 - val hence: (((string * Args.src list) *
11.198 - (string * (string list * string list)) list) * Comment.text) list
11.199 + val presume: ((string * Args.src list) * (string * (string list * string list)) list) list
11.200 -> ProofHistory.T -> ProofHistory.T
11.201 - val hence_i: (((string * Proof.context attribute list) *
11.202 - (term * (term list * term list)) list) * Comment.text) list
11.203 + val presume_i:
11.204 + ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
11.205 -> ProofHistory.T -> ProofHistory.T
11.206 - val show: (((string * Args.src list) *
11.207 - (string * (string list * string list)) list) * Comment.text) list
11.208 + val have: ((string * Args.src list) * (string * (string list * string list)) list) list
11.209 + -> ProofHistory.T -> ProofHistory.T
11.210 + val have_i: ((string * Proof.context attribute list) *
11.211 + (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
11.212 + val hence: ((string * Args.src list) * (string * (string list * string list)) list) list
11.213 + -> ProofHistory.T -> ProofHistory.T
11.214 + val hence_i: ((string * Proof.context attribute list) *
11.215 + (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
11.216 + val show: ((string * Args.src list) * (string * (string list * string list)) list) list
11.217 -> bool -> ProofHistory.T -> ProofHistory.T
11.218 - val show_i: (((string * Proof.context attribute list) *
11.219 - (term * (term list * term list)) list) * Comment.text) list
11.220 + val show_i: ((string * Proof.context attribute list) *
11.221 + (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
11.222 + val thus: ((string * Args.src list) * (string * (string list * string list)) list) list
11.223 -> bool -> ProofHistory.T -> ProofHistory.T
11.224 - val thus: (((string * Args.src list) *
11.225 - (string * (string list * string list)) list) * Comment.text) list
11.226 - -> bool -> ProofHistory.T -> ProofHistory.T
11.227 - val thus_i: (((string * Proof.context attribute list) *
11.228 - (term * (term list * term list)) list) * Comment.text) list
11.229 - -> bool -> ProofHistory.T -> ProofHistory.T
11.230 - val local_def: ((string * Args.src list) * (string * (string * string list)))
11.231 - * Comment.text -> ProofHistory.T -> ProofHistory.T
11.232 - val local_def_i: ((string * Args.src list) * (string * (term * term list)))
11.233 - * Comment.text -> ProofHistory.T -> ProofHistory.T
11.234 - val obtain: ((string list * string option) * Comment.text) list
11.235 - * (((string * Args.src list) * (string * (string list * string list)) list)
11.236 - * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.237 - val obtain_i: ((string list * typ option) * Comment.text) list
11.238 - * (((string * Proof.context attribute list) * (term * (term list * term list)) list)
11.239 - * Comment.text) list -> ProofHistory.T -> ProofHistory.T
11.240 - val begin_block: Comment.text -> ProofHistory.T -> ProofHistory.T
11.241 - val next_block: Comment.text -> ProofHistory.T -> ProofHistory.T
11.242 - val end_block: Comment.text -> ProofHistory.T -> ProofHistory.T
11.243 - val defer: int option * Comment.text -> ProofHistory.T -> ProofHistory.T
11.244 - val prefer: int * Comment.text -> ProofHistory.T -> ProofHistory.T
11.245 - val apply: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
11.246 - val apply_end: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
11.247 - val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
11.248 + val thus_i: ((string * Proof.context attribute list)
11.249 + * (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
11.250 + val local_def: (string * Args.src list) * (string * (string * string list))
11.251 -> ProofHistory.T -> ProofHistory.T
11.252 - val qed: (Method.text * Comment.interest) option * Comment.text
11.253 + val local_def_i: (string * Args.src list) * (string * (term * term list))
11.254 + -> ProofHistory.T -> ProofHistory.T
11.255 + val obtain: (string list * string option) list
11.256 + * ((string * Args.src list) * (string * (string list * string list)) list) list
11.257 + -> ProofHistory.T -> ProofHistory.T
11.258 + val obtain_i: (string list * typ option) list
11.259 + * ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
11.260 + -> ProofHistory.T -> ProofHistory.T
11.261 + val begin_block: ProofHistory.T -> ProofHistory.T
11.262 + val next_block: ProofHistory.T -> ProofHistory.T
11.263 + val end_block: ProofHistory.T -> ProofHistory.T
11.264 + val defer: int option -> ProofHistory.T -> ProofHistory.T
11.265 + val prefer: int -> ProofHistory.T -> ProofHistory.T
11.266 + val apply: Method.text -> ProofHistory.T -> ProofHistory.T
11.267 + val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
11.268 + val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
11.269 + val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
11.270 + val terminal_proof: Method.text * Method.text option
11.271 -> Toplevel.transition -> Toplevel.transition
11.272 - val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
11.273 - * Comment.text -> Toplevel.transition -> Toplevel.transition
11.274 - val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
11.275 - val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
11.276 - val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
11.277 - val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
11.278 - val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
11.279 + val default_proof: Toplevel.transition -> Toplevel.transition
11.280 + val immediate_proof: Toplevel.transition -> Toplevel.transition
11.281 + val done_proof: Toplevel.transition -> Toplevel.transition
11.282 + val skip_proof: Toplevel.transition -> Toplevel.transition
11.283 + val forget_proof: Toplevel.transition -> Toplevel.transition
11.284 val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
11.285 - val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
11.286 - -> Toplevel.transition -> Toplevel.transition
11.287 - val also_i: (thm list * Comment.interest) option * Comment.text
11.288 - -> Toplevel.transition -> Toplevel.transition
11.289 - val finally: ((string * Args.src list) list * Comment.interest) option * Comment.text
11.290 - -> Toplevel.transition -> Toplevel.transition
11.291 - val finally_i: (thm list * Comment.interest) option * Comment.text
11.292 - -> Toplevel.transition -> Toplevel.transition
11.293 - val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
11.294 - val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition
11.295 - val parse_ast_translation: string * Comment.text -> theory -> theory
11.296 - val parse_translation: string * Comment.text -> theory -> theory
11.297 - val print_translation: string * Comment.text -> theory -> theory
11.298 - val typed_print_translation: string * Comment.text -> theory -> theory
11.299 - val print_ast_translation: string * Comment.text -> theory -> theory
11.300 - val token_translation: string * Comment.text -> theory -> theory
11.301 - val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
11.302 - val add_oracle: (bstring * string) * Comment.text -> theory -> theory
11.303 - val add_locale: bstring * Locale.expr * (Args.src Locale.element * Comment.text) list
11.304 - -> theory -> theory
11.305 + val also: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
11.306 + val also_i: thm list option -> Toplevel.transition -> Toplevel.transition
11.307 + val finally: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
11.308 + val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition
11.309 + val moreover: Toplevel.transition -> Toplevel.transition
11.310 + val ultimately: Toplevel.transition -> Toplevel.transition
11.311 + val parse_ast_translation: string -> theory -> theory
11.312 + val parse_translation: string -> theory -> theory
11.313 + val print_translation: string -> theory -> theory
11.314 + val typed_print_translation: string -> theory -> theory
11.315 + val print_ast_translation: string -> theory -> theory
11.316 + val token_translation: string -> theory -> theory
11.317 + val method_setup: bstring * string * string -> theory -> theory
11.318 + val add_oracle: bstring * string -> theory -> theory
11.319 + val add_locale: bstring * Locale.expr * Args.src Locale.element list -> theory -> theory
11.320 val begin_theory: string -> string list -> (string * bool) list -> theory
11.321 val end_theory: theory -> theory
11.322 val kill_theory: string -> unit
11.323 @@ -225,21 +173,20 @@
11.324
11.325 (* markup commands *)
11.326
11.327 -fun add_header comment =
11.328 +fun add_header x =
11.329 Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
11.330
11.331 fun add_text _ x = x;
11.332 fun add_text_raw _ x = x;
11.333
11.334 -fun add_heading add present txt thy =
11.335 - (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy);
11.336 +fun add_heading add present txt thy = (Context.setmp (Some thy) present txt; add txt thy);
11.337
11.338 val add_chapter = add_heading add_text Present.section;
11.339 val add_section = add_heading add_text Present.section;
11.340 val add_subsection = add_heading add_text Present.subsection;
11.341 val add_subsubsection = add_heading add_text Present.subsubsection;
11.342
11.343 -fun add_txt (_: Comment.text) = ProofHistory.apply I;
11.344 +fun add_txt (_: string) = ProofHistory.apply I;
11.345 val add_txt_raw = add_txt;
11.346 val add_sect = add_txt;
11.347 val add_subsect = add_txt;
11.348 @@ -248,9 +195,6 @@
11.349
11.350 (* name spaces *)
11.351
11.352 -fun global_path comment_ignore = PureThy.global_path;
11.353 -fun local_path comment_ignore = PureThy.local_path;
11.354 -
11.355 local
11.356
11.357 val kinds =
11.358 @@ -259,7 +203,7 @@
11.359 can (Sign.certify_tycon sg) c orelse can (Sign.certify_tyabbr sg) c),
11.360 (Sign.constK, can o Sign.certify_const)];
11.361
11.362 -fun gen_hide intern ((kind, xnames), comment_ignore) thy =
11.363 +fun gen_hide intern (kind, xnames) thy =
11.364 (case assoc (kinds, kind) of
11.365 Some check =>
11.366 let
11.367 @@ -280,51 +224,27 @@
11.368 end;
11.369
11.370
11.371 -(* signature and syntax *)
11.372 -
11.373 -val add_classes = Theory.add_classes o Comment.ignore;
11.374 -val add_classes_i = Theory.add_classes_i o Comment.ignore;
11.375 -val add_classrel = Theory.add_classrel o single o Comment.ignore;
11.376 -val add_classrel_i = Theory.add_classrel_i o single o Comment.ignore;
11.377 -val add_defsort = Theory.add_defsort o Comment.ignore;
11.378 -val add_defsort_i = Theory.add_defsort_i o Comment.ignore;
11.379 -val add_nonterminals = Theory.add_nonterminals o map Comment.ignore;
11.380 -val add_tyabbrs = Theory.add_tyabbrs o map Comment.ignore;
11.381 -val add_tyabbrs_i = Theory.add_tyabbrs_i o map Comment.ignore;
11.382 -val add_arities = Theory.add_arities o map Comment.ignore;
11.383 -val add_arities_i = Theory.add_arities_i o map Comment.ignore;
11.384 -val add_typedecl = PureThy.add_typedecls o single o Comment.ignore;
11.385 -val add_consts = Theory.add_consts o map Comment.ignore;
11.386 -val add_consts_i = Theory.add_consts_i o map Comment.ignore;
11.387 -fun add_modesyntax mode = Theory.add_modesyntax mode o map Comment.ignore;
11.388 -fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
11.389 -val add_trrules = Theory.add_trrules o map Comment.ignore;
11.390 -val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
11.391 -val add_judgment = ObjectLogic.add_judgment o Comment.ignore;
11.392 -val add_judgment_i = ObjectLogic.add_judgment_i o Comment.ignore;
11.393 -
11.394 -
11.395 (* axioms and defs *)
11.396
11.397 fun add_axms f args thy =
11.398 f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
11.399
11.400 -val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
11.401 -val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
11.402 -fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) (map Comment.ignore args);
11.403 -fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) (map Comment.ignore args);
11.404 +val add_axioms = add_axms (#1 oo PureThy.add_axioms);
11.405 +val add_axioms_i = #1 oo PureThy.add_axioms_i;
11.406 +fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args;
11.407 +fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args;
11.408
11.409
11.410 (* constdefs *)
11.411
11.412 fun gen_add_constdefs consts defs args thy =
11.413 thy
11.414 - |> consts (map (Comment.ignore o fst) args)
11.415 - |> defs (false, map (fn (((c, _, mx), _), (s, _)) =>
11.416 - (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
11.417 + |> consts (map fst args)
11.418 + |> defs (false, map (fn ((c, _, mx), s) =>
11.419 + ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
11.420
11.421 -fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args;
11.422 -fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args;
11.423 +val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;
11.424 +val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;
11.425
11.426
11.427 (* attributes *)
11.428 @@ -355,30 +275,27 @@
11.429
11.430 in
11.431
11.432 -fun theorems_i k = (present_thmss k oo PureThy.have_thmss_i (Drule.kind k)) o map Comment.ignore;
11.433 -fun locale_theorems_i k loc = (present_thmss k oo Locale.have_thmss_i k loc) o map Comment.ignore;
11.434 +fun theorems_i k = present_thmss k oo PureThy.have_thmss_i (Drule.kind k);
11.435 +fun locale_theorems_i k loc = present_thmss k oo Locale.have_thmss_i k loc;
11.436
11.437 fun theorems k args thy = thy
11.438 - |> PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args))
11.439 + |> PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
11.440 |> present_thmss k;
11.441
11.442 fun locale_theorems k loc args thy = thy
11.443 - |> Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args))
11.444 + |> Locale.have_thmss k loc (local_attribs thy args)
11.445 |> present_thmss k;
11.446
11.447 fun smart_theorems k opt_loc args thy = thy
11.448 |> (case opt_loc of
11.449 - None => PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args))
11.450 - | Some loc => Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args)))
11.451 + None => PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
11.452 + | Some loc => Locale.have_thmss k loc (local_attribs thy args))
11.453 |> present_thmss k;
11.454
11.455 -fun declare_theorems opt_loc (args, comment) =
11.456 - #1 o smart_theorems "" opt_loc [((("", []), args), comment)];
11.457 +fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
11.458
11.459 -fun apply_theorems args =
11.460 - apsnd (flat o map snd) o theorems "" [((("", []), args), Comment.none)];
11.461 -fun apply_theorems_i args =
11.462 - apsnd (flat o map snd) o theorems_i "" [((("", []), args), Comment.none)];
11.463 +fun apply_theorems args = apsnd (flat o map snd) o theorems "" [(("", []), args)];
11.464 +fun apply_theorems_i args = apsnd (flat o map snd) o theorems_i "" [(("", []), args)];
11.465
11.466 end;
11.467
11.468 @@ -391,25 +308,25 @@
11.469
11.470 fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
11.471
11.472 -val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss o map Comment.ignore;
11.473 -val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i o map Comment.ignore;
11.474 -val from_facts = chain_thmss (local_thmss Proof.have_thmss) o map Comment.ignore;
11.475 -val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i) o map Comment.ignore;
11.476 -val with_facts = chain_thmss (local_thmss Proof.with_thmss) o map Comment.ignore;
11.477 -val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i) o map Comment.ignore;
11.478 -fun chain comment_ignore = ProofHistory.apply Proof.chain;
11.479 +val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss;
11.480 +val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i;
11.481 +val from_facts = chain_thmss (local_thmss Proof.have_thmss);
11.482 +val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i);
11.483 +val with_facts = chain_thmss (local_thmss Proof.with_thmss);
11.484 +val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i);
11.485 +val chain = ProofHistory.apply Proof.chain;
11.486
11.487
11.488 (* context *)
11.489
11.490 -val fix = ProofHistory.apply o Proof.fix o map Comment.ignore;
11.491 -val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
11.492 -val let_bind = ProofHistory.apply o Proof.let_bind o map Comment.ignore;
11.493 -val let_bind_i = ProofHistory.apply o Proof.let_bind_i o map Comment.ignore;
11.494 +val fix = ProofHistory.apply o Proof.fix;
11.495 +val fix_i = ProofHistory.apply o Proof.fix_i;
11.496 +val let_bind = ProofHistory.apply o Proof.let_bind;
11.497 +val let_bind_i = ProofHistory.apply o Proof.let_bind_i;
11.498
11.499 -fun invoke_case ((name, xs, src), comment_ignore) = ProofHistory.apply (fn state =>
11.500 +fun invoke_case (name, xs, src) = ProofHistory.apply (fn state =>
11.501 Proof.invoke_case (name, xs, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
11.502 -val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
11.503 +val invoke_case_i = ProofHistory.apply o Proof.invoke_case;
11.504
11.505
11.506 (* local results *)
11.507 @@ -487,94 +404,80 @@
11.508
11.509 fun multi_theorem k a elems args int thy =
11.510 global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a) None
11.511 - (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy;
11.512 + (map (Locale.attribute (Attrib.local_attribute thy)) elems)) args int thy;
11.513
11.514 -fun multi_theorem_i k a elems =
11.515 - global_statement_i (Proof.multi_theorem_i k a None elems) o map Comment.ignore;
11.516 +fun multi_theorem_i k a elems = global_statement_i (Proof.multi_theorem_i k a None elems);
11.517
11.518 fun locale_multi_theorem k a locale elems args int thy =
11.519 global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a)
11.520 - (Some (locale, map (map (Attrib.local_attribute thy) o snd o fst o Comment.ignore) args))
11.521 + (Some (locale, map (map (Attrib.local_attribute thy) o snd o fst) args))
11.522 (map (Locale.attribute (Attrib.local_attribute thy)) elems))
11.523 - (map (apfst (apsnd (K [])) o Comment.ignore) args) int thy;
11.524 + (map (apfst (apsnd (K []))) args) int thy;
11.525
11.526 fun locale_multi_theorem_i k a locale elems args =
11.527 - global_statement_i (Proof.multi_theorem_i k a
11.528 - (Some (locale, map (snd o fst o Comment.ignore) args)) elems)
11.529 - (map (apfst (apsnd (K [])) o Comment.ignore) args);
11.530 + global_statement_i (Proof.multi_theorem_i k a (Some (locale, map (snd o fst) args)) elems)
11.531 + (map (apfst (apsnd (K []))) args);
11.532
11.533 -fun theorem k ((a, t), cmt) = multi_theorem k a [] [((("", []), [t]), cmt)];
11.534 -fun theorem_i k ((a, t), cmt) = multi_theorem_i k a [] [((("", []), [t]), cmt)];
11.535 +fun theorem k (a, t) = multi_theorem k a [] [(("", []), [t])];
11.536 +fun theorem_i k (a, t) = multi_theorem_i k a [] [(("", []), [t])];
11.537
11.538 fun smart_multi_theorem k a (None, elems) = multi_theorem k a elems
11.539 | smart_multi_theorem k a (Some locale, elems) = locale_multi_theorem k a locale elems;
11.540
11.541 -val assume = local_statement Proof.assume I o map Comment.ignore;
11.542 -val assume_i = local_statement_i Proof.assume_i I o map Comment.ignore;
11.543 -val presume = local_statement Proof.presume I o map Comment.ignore;
11.544 -val presume_i = local_statement_i Proof.presume_i I o map Comment.ignore;
11.545 -val have = local_statement (Proof.have Seq.single) I o map Comment.ignore;
11.546 -val have_i = local_statement_i (Proof.have_i Seq.single) I o map Comment.ignore;
11.547 -val hence = local_statement (Proof.have Seq.single) Proof.chain o map Comment.ignore;
11.548 -val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o map Comment.ignore;
11.549 -val show = local_statement' (Proof.show check_goal Seq.single) I o map Comment.ignore;
11.550 -val show_i = local_statement_i' (Proof.show_i check_goal Seq.single) I o map Comment.ignore;
11.551 -val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain o map Comment.ignore;
11.552 -val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain o map Comment.ignore;
11.553 +val assume = local_statement Proof.assume I;
11.554 +val assume_i = local_statement_i Proof.assume_i I;
11.555 +val presume = local_statement Proof.presume I;
11.556 +val presume_i = local_statement_i Proof.presume_i I;
11.557 +val have = local_statement (Proof.have Seq.single) I;
11.558 +val have_i = local_statement_i (Proof.have_i Seq.single) I;
11.559 +val hence = local_statement (Proof.have Seq.single) Proof.chain;
11.560 +val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain;
11.561 +val show = local_statement' (Proof.show check_goal Seq.single) I;
11.562 +val show_i = local_statement_i' (Proof.show_i check_goal Seq.single) I;
11.563 +val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain;
11.564 +val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain;
11.565
11.566 fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state =>
11.567 f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state);
11.568
11.569 -val local_def = gen_def Proof.def o Comment.ignore;
11.570 -val local_def_i = gen_def Proof.def_i o Comment.ignore;
11.571 +val local_def = gen_def Proof.def;
11.572 +val local_def_i = gen_def Proof.def_i;
11.573
11.574 fun obtain (xs, asms) = ProofHistory.applys (fn state =>
11.575 - Obtain.obtain (map Comment.ignore xs)
11.576 - (map (local_attributes' state) (map Comment.ignore asms)) state);
11.577 + Obtain.obtain xs (map (local_attributes' state) asms) state);
11.578
11.579 -fun obtain_i (xs, asms) = ProofHistory.applys (fn state =>
11.580 - Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms) state);
11.581 +fun obtain_i (xs, asms) = ProofHistory.applys (Obtain.obtain_i xs asms);
11.582
11.583 end;
11.584
11.585
11.586 (* blocks *)
11.587
11.588 -fun begin_block comment_ignore = ProofHistory.apply Proof.begin_block;
11.589 -fun next_block comment_ignore = ProofHistory.apply Proof.next_block;
11.590 -fun end_block comment_ignore = ProofHistory.applys Proof.end_block;
11.591 +val begin_block = ProofHistory.apply Proof.begin_block;
11.592 +val next_block = ProofHistory.apply Proof.next_block;
11.593 +val end_block = ProofHistory.applys Proof.end_block;
11.594
11.595
11.596 (* shuffle state *)
11.597
11.598 fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
11.599
11.600 -fun defer (i, comment_ignore) = ProofHistory.applys (shuffle Method.defer i);
11.601 -fun prefer (i, comment_ignore) = ProofHistory.applys (shuffle Method.prefer i);
11.602 +fun defer i = ProofHistory.applys (shuffle Method.defer i);
11.603 +fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
11.604
11.605
11.606 (* backward steps *)
11.607
11.608 -fun apply (m, comment_ignore) = ProofHistory.applys
11.609 +fun apply m = ProofHistory.applys
11.610 (Seq.map (Proof.goal_facts (K [])) o Method.refine m o Proof.assert_backward);
11.611 -
11.612 -fun apply_end (m, comment_ignore) = ProofHistory.applys
11.613 - (Method.refine_end m o Proof.assert_forward);
11.614 -
11.615 -val proof = ProofHistory.applys o Method.proof o
11.616 - apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;
11.617 +fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
11.618 +val proof = ProofHistory.applys o Method.proof;
11.619
11.620
11.621 (* local endings *)
11.622
11.623 -val local_qed =
11.624 - proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest;
11.625 -
11.626 -fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
11.627 -
11.628 -val local_terminal_proof =
11.629 - proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
11.630 -
11.631 +val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true);
11.632 +val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof);
11.633 val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
11.634 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
11.635 val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
11.636 @@ -596,9 +499,8 @@
11.637 thy
11.638 end);
11.639
11.640 -fun global_qed m = global_result (K (Method.global_qed true (apsome Comment.ignore_interest m)));
11.641 -fun global_terminal_proof m =
11.642 - global_result (K (Method.global_terminal_proof (ignore_interests m)));
11.643 +fun global_qed m = global_result (K (Method.global_qed true m));
11.644 +fun global_terminal_proof m = global_result (K (Method.global_terminal_proof m));
11.645 val global_default_proof = global_result (K Method.global_default_proof);
11.646 val global_immediate_proof = global_result (K Method.global_immediate_proof);
11.647 val global_skip_proof = global_result SkipProof.global_skip_proof;
11.648 @@ -607,14 +509,13 @@
11.649
11.650 (* common endings *)
11.651
11.652 -fun qed (meth, comment) = local_qed meth o global_qed meth;
11.653 -fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
11.654 -fun default_proof comment = local_default_proof o global_default_proof;
11.655 -fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
11.656 -fun done_proof comment = local_done_proof o global_done_proof;
11.657 -fun skip_proof comment = local_skip_proof o global_skip_proof;
11.658 -
11.659 -fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
11.660 +fun qed meth = local_qed meth o global_qed meth;
11.661 +fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
11.662 +val default_proof = local_default_proof o global_default_proof;
11.663 +val immediate_proof = local_immediate_proof o global_immediate_proof;
11.664 +val done_proof = local_done_proof o global_done_proof;
11.665 +val skip_proof = local_skip_proof o global_skip_proof;
11.666 +val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
11.667
11.668
11.669 (* calculational proof commands *)
11.670 @@ -628,8 +529,8 @@
11.671
11.672 fun proof''' f = Toplevel.proof' (f o cond_print_calc);
11.673
11.674 -fun gen_calc get f (args, _) prt state =
11.675 - f (apsome (fn (srcs, _) => get srcs state) args) prt state;
11.676 +fun gen_calc get f args prt state =
11.677 + f (apsome (fn srcs => get srcs state) args) prt state;
11.678
11.679 in
11.680
11.681 @@ -640,8 +541,8 @@
11.682 fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
11.683 fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
11.684 fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
11.685 -fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
11.686 -fun ultimately comment = proof''' (ProofHistory.apply o Calculation.ultimately);
11.687 +val moreover = proof''' (ProofHistory.apply o Calculation.moreover);
11.688 +val ultimately = proof''' (ProofHistory.apply o Calculation.ultimately);
11.689
11.690 end;
11.691
11.692 @@ -650,32 +551,32 @@
11.693
11.694 val parse_ast_translation =
11.695 Context.use_let "val parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
11.696 - "Theory.add_trfuns (parse_ast_translation, [], [], [])" o Comment.ignore;
11.697 + "Theory.add_trfuns (parse_ast_translation, [], [], [])";
11.698
11.699 val parse_translation =
11.700 Context.use_let "val parse_translation: (string * (term list -> term)) list"
11.701 - "Theory.add_trfuns ([], parse_translation, [], [])" o Comment.ignore;
11.702 + "Theory.add_trfuns ([], parse_translation, [], [])";
11.703
11.704 val print_translation =
11.705 Context.use_let "val print_translation: (string * (term list -> term)) list"
11.706 - "Theory.add_trfuns ([], [], print_translation, [])" o Comment.ignore;
11.707 + "Theory.add_trfuns ([], [], print_translation, [])";
11.708
11.709 val print_ast_translation =
11.710 Context.use_let "val print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
11.711 - "Theory.add_trfuns ([], [], [], print_ast_translation)" o Comment.ignore;
11.712 + "Theory.add_trfuns ([], [], [], print_ast_translation)";
11.713
11.714 val typed_print_translation =
11.715 Context.use_let "val typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
11.716 - "Theory.add_trfunsT typed_print_translation" o Comment.ignore;
11.717 + "Theory.add_trfunsT typed_print_translation";
11.718
11.719 val token_translation =
11.720 Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
11.721 - "Theory.add_tokentrfuns token_translation" o Comment.ignore;
11.722 + "Theory.add_tokentrfuns token_translation";
11.723
11.724
11.725 (* add method *)
11.726
11.727 -fun method_setup ((name, txt, cmt), comment_ignore) =
11.728 +fun method_setup (name, txt, cmt) =
11.729 Context.use_let
11.730 "val thm = PureThy.get_thm_closure (Context.the_context ());\n\
11.731 \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
11.732 @@ -686,7 +587,7 @@
11.733
11.734 (* add_oracle *)
11.735
11.736 -fun add_oracle ((name, txt), comment_ignore) =
11.737 +fun add_oracle (name, txt) =
11.738 Context.use_let
11.739 "val oracle: bstring * (Sign.sg * Object.T -> term)"
11.740 "Theory.add_oracle oracle"
11.741 @@ -696,8 +597,7 @@
11.742 (* add_locale *)
11.743
11.744 fun add_locale (name, import, body) thy =
11.745 - Locale.add_locale name import
11.746 - (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body) thy;
11.747 + Locale.add_locale name import (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
11.748
11.749
11.750 (* theory init and exit *)
12.1 --- a/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:25:58 2002 +0100
12.2 +++ b/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:28:27 2002 +0100
12.3 @@ -45,9 +45,6 @@
12.4 val xname: token list -> xstring * token list
12.5 val text: token list -> string * token list
12.6 val uname: token list -> string option * token list
12.7 - val comment: token list -> Comment.text * token list
12.8 - val marg_comment: token list -> Comment.text * token list
12.9 - val interest: token list -> Comment.interest * token list
12.10 val sort: token list -> string * token list
12.11 val arity: token list -> (string list * string) * token list
12.12 val simple_arity: token list -> (string list * xclass) * token list
12.13 @@ -177,15 +174,6 @@
12.14 val uname = underscore >> K None || name >> Some;
12.15
12.16
12.17 -(* formal comments *)
12.18 -
12.19 -val comment = text >> (Comment.plain o Library.single);
12.20 -val marg_comment = Scan.repeat ($$$ "--" |-- text) >> Comment.plain;
12.21 -
12.22 -val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
12.23 - $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;
12.24 -
12.25 -
12.26 (* sorts and arities *)
12.27
12.28 val sort = group "sort" xname;
13.1 --- a/src/Pure/Isar/outer_syntax.ML Tue Feb 12 20:25:58 2002 +0100
13.2 +++ b/src/Pure/Isar/outer_syntax.ML Tue Feb 12 20:28:27 2002 +0100
13.3 @@ -228,20 +228,19 @@
13.4
13.5 (* basic sources *)
13.6
13.7 -fun token_source (src, pos) =
13.8 - src
13.9 - |> Symbol.source false
13.10 - |> T.source false (K (get_lexicons ())) pos;
13.11 -
13.12 fun toplevel_source term do_recover cmd src =
13.13 let
13.14 val no_terminator =
13.15 Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
13.16 - val recover = Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None];
13.17 + fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]) x;
13.18 in
13.19 src
13.20 + |> T.source_proper
13.21 |> Source.source T.stopper
13.22 - (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
13.23 + (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some))
13.24 + (if do_recover then Some recover else None)
13.25 + |> Source.mapfilter I
13.26 + |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
13.27 (if do_recover then Some recover else None)
13.28 |> Source.mapfilter I
13.29 end;
13.30 @@ -254,7 +253,6 @@
13.31 |> Symbol.source true
13.32 |> T.source true get_lexicons
13.33 (if no_pos then Position.none else Position.line_name 1 "stdin")
13.34 - |> T.source_proper
13.35 |> toplevel_source term true get_parser;
13.36
13.37
13.38 @@ -294,7 +292,6 @@
13.39
13.40 fun parse_thy src =
13.41 src
13.42 - |> T.source_proper
13.43 |> toplevel_source false false (K (get_parser ()))
13.44 |> Source.exhaust;
13.45
13.46 @@ -311,7 +308,10 @@
13.47 Present.old_symbol_source name present_text) (*note: text presented twice*)
13.48 else
13.49 let
13.50 - val tok_src = Source.exhausted (token_source (text_src, pos));
13.51 + val tok_src = text_src
13.52 + |> Symbol.source false
13.53 + |> T.source false (K (get_lexicons ())) pos
13.54 + |> Source.exhausted;
13.55 val out = Toplevel.excursion_result
13.56 (IsarOutput.parse_thy markup (#1 (get_lexicons ()))
13.57 (parse_thy tok_src) tok_src);
14.1 --- a/src/Pure/axclass.ML Tue Feb 12 20:25:58 2002 +0100
14.2 +++ b/src/Pure/axclass.ML Tue Feb 12 20:28:27 2002 +0100
14.3 @@ -26,12 +26,10 @@
14.4 val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
14.5 val default_intro_classes_tac: thm list -> int -> tactic
14.6 val axclass_tac: thm list -> tactic
14.7 - val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
14.8 - val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
14.9 - val instance_arity_proof: (xstring * string list * xclass) * Comment.text
14.10 - -> bool -> theory -> ProofHistory.T
14.11 - val instance_arity_proof_i: (string * sort list * class) * Comment.text
14.12 - -> bool -> theory -> ProofHistory.T
14.13 + val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
14.14 + val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
14.15 + val instance_arity_proof: xstring * string list * xclass -> bool -> theory -> ProofHistory.T
14.16 + val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
14.17 val setup: (theory -> theory) list
14.18 end;
14.19
14.20 @@ -421,10 +419,10 @@
14.21
14.22 fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
14.23
14.24 -fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
14.25 +fun inst_proof mk_prop add_thms sig_prop int thy =
14.26 thy
14.27 - |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
14.28 - (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
14.29 + |> IsarThy.theorem_i Drule.internalK (("", [inst_attribute add_thms]),
14.30 + (mk_prop (Theory.sign_of thy) sig_prop, ([], []))) int;
14.31
14.32 val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
14.33 val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
14.34 @@ -448,17 +446,14 @@
14.35
14.36 val axclassP =
14.37 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
14.38 - (((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
14.39 - P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
14.40 - -- Scan.repeat (P.spec_name --| P.marg_comment)
14.41 + ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
14.42 + P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
14.43 >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
14.44
14.45 val instanceP =
14.46 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
14.47 - ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname)
14.48 - -- P.marg_comment >> instance_subclass_proof ||
14.49 - (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment
14.50 - >> instance_arity_proof)
14.51 + ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof ||
14.52 + (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) >> instance_arity_proof)
14.53 >> (Toplevel.print oo Toplevel.theory_to_proof));
14.54
14.55 val _ = OuterSyntax.add_parsers [axclassP, instanceP];
15.1 --- a/src/ZF/Tools/datatype_package.ML Tue Feb 12 20:25:58 2002 +0100
15.2 +++ b/src/ZF/Tools/datatype_package.ML Tue Feb 12 20:28:27 2002 +0100
15.3 @@ -419,14 +419,14 @@
15.4
15.5 val con_decl =
15.6 P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
15.7 - --| P.marg_comment >> P.triple1;
15.8 + >> P.triple1;
15.9
15.10 val datatype_decl =
15.11 - (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term --| P.marg_comment) "") --
15.12 + (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
15.13 P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
15.14 - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
15.15 - Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
15.16 - Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
15.17 + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
15.18 + Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
15.19 + Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
15.20 >> (Toplevel.theory o mk_datatype);
15.21
15.22 val coind_prefix = if coind then "co" else "";
16.1 --- a/src/ZF/Tools/ind_cases.ML Tue Feb 12 20:25:58 2002 +0100
16.2 +++ b/src/ZF/Tools/ind_cases.ML Tue Feb 12 20:28:27 2002 +0100
16.3 @@ -55,8 +55,8 @@
16.4 val read_prop = ProofContext.read_prop (ProofContext.init thy);
16.5 val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
16.6 val facts = args |> map (fn ((name, srcs), props) =>
16.7 - (((name, map (Attrib.global_attribute thy) srcs),
16.8 - map (Thm.no_attributes o single o mk_cases) props), Comment.none));
16.9 + ((name, map (Attrib.global_attribute thy) srcs),
16.10 + map (Thm.no_attributes o single o mk_cases) props));
16.11 in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
16.12
16.13
16.14 @@ -84,7 +84,7 @@
16.15 local structure P = OuterParse and K = OuterSyntax.Keyword in
16.16
16.17 val ind_cases =
16.18 - P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment)
16.19 + P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
16.20 >> (Toplevel.theory o inductive_cases);
16.21
16.22 val inductive_casesP =
17.1 --- a/src/ZF/Tools/inductive_package.ML Tue Feb 12 20:25:58 2002 +0100
17.2 +++ b/src/ZF/Tools/inductive_package.ML Tue Feb 12 20:28:27 2002 +0100
17.3 @@ -605,13 +605,13 @@
17.4
17.5 val ind_decl =
17.6 (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
17.7 - ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term)) --| P.marg_comment) --
17.8 + ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) --
17.9 (P.$$$ "intros" |--
17.10 - P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
17.11 - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
17.12 - Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
17.13 - Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
17.14 - Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
17.15 + P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
17.16 + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
17.17 + Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] --
17.18 + Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
17.19 + Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
17.20 >> (Toplevel.theory o mk_ind);
17.21
17.22 val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
18.1 --- a/src/ZF/Tools/primrec_package.ML Tue Feb 12 20:25:58 2002 +0100
18.2 +++ b/src/ZF/Tools/primrec_package.ML Tue Feb 12 20:28:27 2002 +0100
18.3 @@ -202,7 +202,7 @@
18.4
18.5 local structure P = OuterParse and K = OuterSyntax.Keyword in
18.6
18.7 -val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
18.8 +val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
18.9
18.10 val primrecP =
18.11 OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl