--- a/src/HOL/Tools/datatype_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -858,12 +858,13 @@
val datatype_decl =
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment));
+ (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
fun mk_datatype args =
let
val names = map (fn ((((None, _), t), _), _) => t | ((((Some t, _), _), _), _) => t) args;
- val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
+ val specs = map (fn ((((_, vs), t), mx), cons) =>
+ (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
in #1 o add_datatype false names specs end;
val datatypeP =
--- a/src/HOL/Tools/inductive_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -44,10 +44,8 @@
val inductive_forall_name: string
val inductive_forall_def: thm
val rulify: thm -> thm
- val inductive_cases: (((bstring * Args.src list) * string list) * Comment.text) list
- -> theory -> theory
- val inductive_cases_i: (((bstring * theory attribute list) * term list) * Comment.text) list
- -> theory -> theory
+ val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
+ val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
@@ -587,8 +585,8 @@
val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
- val facts = args |> map (fn (((a, atts), props), comment) =>
- (((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props), comment));
+ val facts = args |> map (fn ((a, atts), props) =>
+ ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
@@ -874,10 +872,10 @@
#1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
fun ind_decl coind =
- (Scan.repeat1 P.term --| P.marg_comment) --
+ Scan.repeat1 P.term --
(P.$$$ "intros" |--
- P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
- Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) []
+ P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
+ Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
>> (Toplevel.theory o mk_ind coind);
val inductiveP =
@@ -888,7 +886,7 @@
val ind_cases =
- P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment)
+ P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
>> (Toplevel.theory o inductive_cases);
val inductive_casesP =
--- a/src/HOL/Tools/primrec_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/primrec_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -291,7 +291,7 @@
val primrec_decl =
Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
+ Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
val primrecP =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
--- a/src/HOL/Tools/recdef_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/recdef_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -310,8 +310,8 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- thy |> IsarThy.theorem_i Drule.internalK
- (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
+ thy
+ |> IsarThy.theorem_i Drule.internalK ((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))) int
end;
val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
@@ -340,8 +340,7 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment)
- -- Scan.option hints
+ P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop) -- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
val recdefP =
@@ -360,8 +359,7 @@
val recdef_tc_decl =
- P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
- --| P.marg_comment;
+ P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")");
fun mk_recdef_tc ((thm_name, name), i) = recdef_tc thm_name name i;
--- a/src/HOL/Tools/record_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/record_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -1086,8 +1086,8 @@
local structure P = OuterParse and K = OuterSyntax.Keyword in
val record_decl =
- P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+")
- -- Scan.repeat1 (P.const --| P.marg_comment));
+ P.type_args -- P.name --
+ (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
val recordP =
OuterSyntax.command "record" "define extensible record" K.thy_decl
--- a/src/HOL/Tools/typedef_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/typedef_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -22,11 +22,9 @@
{type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm}
- val typedef_proof:
- (string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text
+ val typedef_proof: string * (bstring * string list * mixfix) * string * (string * string) option
-> bool -> theory -> ProofHistory.T
- val typedef_proof_i:
- (string * (bstring * string list * mixfix) * term * (string * string) option) * Comment.text
+ val typedef_proof_i: string * (bstring * string list * mixfix) * term * (string * string) option
-> bool -> theory -> ProofHistory.T
end;
@@ -241,15 +239,12 @@
(* typedef_proof interface *)
-fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy =
+fun gen_typedef_proof prep_term (name, typ, set, opt_morphs) int thy =
let
val (_, goal, goal_pat, att_result) =
prepare_typedef prep_term true name typ set opt_morphs thy;
val att = #1 o att_result;
- in
- thy
- |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
- end;
+ in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end;
val typedef_proof = gen_typedef_proof read_term;
val typedef_proof_i = gen_typedef_proof cert_term;
@@ -262,18 +257,17 @@
val typedeclP =
OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
- (P.type_args -- P.name -- P.opt_infix --| P.marg_comment >> (fn ((vs, t), mx) =>
+ (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
Toplevel.theory (add_typedecls [(t, vs, mx)])));
val typedef_proof_decl =
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
(P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)) --
- P.marg_comment;
+ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
-fun mk_typedef_proof (((((opt_name, (vs, t)), mx), A), morphs), comment) =
- typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs), comment);
+fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), morphs) =
+ typedef_proof (if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs);
val typedefP =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
@@ -285,5 +279,4 @@
end;
-
end;
--- a/src/HOLCF/cont_consts.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOLCF/cont_consts.ML Tue Feb 12 20:28:27 2002 +0100
@@ -110,7 +110,7 @@
thy
|> consts (map fst args)
|> defs (false, map (fn ((c, _, mx), s) =>
- (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
+ ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args;
fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args;
@@ -122,12 +122,11 @@
val constsP =
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 (P.const --| P.marg_comment) >> (Toplevel.theory o add_consts));
+ (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
val constdefsP =
OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl
- (Scan.repeat1 ((P.const --| P.marg_comment) -- (P.term --| P.marg_comment))
- >> (Toplevel.theory o add_constdefs));
+ (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs));
val _ = OuterSyntax.add_parsers [constsP, constdefsP];
--- a/src/HOLCF/domain/extender.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOLCF/domain/extender.ML Tue Feb 12 20:28:27 2002 +0100
@@ -124,7 +124,7 @@
P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1;
val cons_decl =
- P.name -- Scan.repeat dest_decl -- P.opt_mixfix --| P.marg_comment
+ P.name -- Scan.repeat dest_decl -- P.opt_mixfix
>> (fn ((c, ds), mx) => (c, mx, ds));
val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
--- a/src/Pure/Isar/isar_cmd.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Feb 12 20:28:27 2002 +0100
@@ -29,11 +29,10 @@
val undo_theory: Toplevel.transition -> Toplevel.transition
val undo: Toplevel.transition -> Toplevel.transition
val kill: Toplevel.transition -> Toplevel.transition
- val back: bool * Comment.text -> Toplevel.transition -> Toplevel.transition
- val use: string * Comment.text -> Toplevel.transition -> Toplevel.transition
- val use_mltext_theory: string * Comment.text -> Toplevel.transition -> Toplevel.transition
- val use_mltext: bool -> string * Comment.text -> Toplevel.transition -> Toplevel.transition
- val use_setup: string * Comment.text -> theory -> theory
+ val back: bool -> Toplevel.transition -> Toplevel.transition
+ val use: string -> Toplevel.transition -> Toplevel.transition
+ val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
+ val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
val use_commit: Toplevel.transition -> Toplevel.transition
val cd: string -> Toplevel.transition -> Toplevel.transition
val pwd: Toplevel.transition -> Toplevel.transition
@@ -47,7 +46,7 @@
val print_syntax: Toplevel.transition -> Toplevel.transition
val print_theorems: Toplevel.transition -> Toplevel.transition
val print_locales: Toplevel.transition -> Toplevel.transition
- val print_locale: Locale.expr * (Args.src Locale.element * Comment.text) list
+ val print_locale: Locale.expr * Args.src Locale.element list
-> Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
val print_rules: Toplevel.transition -> Toplevel.transition
@@ -60,16 +59,13 @@
val print_binds: Toplevel.transition -> Toplevel.transition
val print_lthms: Toplevel.transition -> Toplevel.transition
val print_cases: Toplevel.transition -> Toplevel.transition
- val print_thms: (string list * (string * Args.src list) list) * Comment.text
+ val print_thms: string list * (string * Args.src list) list
-> Toplevel.transition -> Toplevel.transition
- val print_prfs: bool -> (string list * (string * Args.src list) list option) * Comment.text
+ val print_prfs: bool -> string list * (string * Args.src list) list option
-> Toplevel.transition -> Toplevel.transition
- val print_prop: (string list * string) * Comment.text
- -> Toplevel.transition -> Toplevel.transition
- val print_term: (string list * string) * Comment.text
- -> Toplevel.transition -> Toplevel.transition
- val print_type: (string list * string) * Comment.text
- -> Toplevel.transition -> Toplevel.transition
+ val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
+ val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
+ val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
end;
structure IsarCmd: ISAR_CMD =
@@ -135,26 +131,23 @@
val undo = Toplevel.kill o undo_theory o undos_proof 1;
val kill = Toplevel.kill o kill_proof;
-
-val back = Toplevel.proof o ProofHistory.back o Comment.ignore;
+val back = Toplevel.proof o ProofHistory.back;
(* use ML text *)
-fun use (name, comment_ignore) = Toplevel.keep (fn state =>
+fun use name = Toplevel.keep (fn state =>
Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
(*passes changes of theory context*)
-val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore;
+val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
(*ignore result theory context*)
-fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state =>
+fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
(Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
-val use_setup = Context.use_setup o Comment.ignore;
-
(*Note: commit is dynamically bound*)
-val use_commit = use_mltext false ("commit();", Comment.none);
+val use_commit = use_mltext false "commit();";
(* current working directory *)
@@ -196,8 +189,7 @@
fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
let val thy = Toplevel.theory_of state in
- Locale.print_locale thy import
- (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body)
+ Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body)
end);
val print_attributes = Toplevel.unknown_theory o
@@ -291,11 +283,10 @@
fun print_item string_of (x, y) = Toplevel.keep (fn state =>
writeln (string_of (Toplevel.enter_forward_proof state) x y));
-val print_thms = print_item string_of_thms o Comment.ignore;
-fun print_prfs full = print_item (string_of_prfs full) o Comment.ignore;
-val print_prop = print_item string_of_prop o Comment.ignore;
-val print_term = print_item string_of_term o Comment.ignore;
-val print_type = print_item string_of_type o Comment.ignore;
-
+val print_thms = print_item string_of_thms;
+fun print_prfs full = print_item (string_of_prfs full);
+val print_prop = print_item string_of_prop;
+val print_term = print_item string_of_term;
+val print_type = print_item string_of_type;
end;
--- a/src/Pure/Isar/isar_syn.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Feb 12 20:28:27 2002 +0100
@@ -37,45 +37,45 @@
(** markup commands **)
val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag
- (P.comment >> IsarThy.add_header);
+ (P.text >> IsarThy.add_header);
val chapterP = OuterSyntax.markup_command IsarOutput.Markup "chapter" "chapter heading"
- K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
+ K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_chapter));
val sectionP = OuterSyntax.markup_command IsarOutput.Markup "section" "section heading"
- K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_section));
+ K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_section));
val subsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsection" "subsection heading"
- K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
+ K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_subsection));
val subsubsectionP =
OuterSyntax.markup_command IsarOutput.Markup "subsubsection" "subsubsection heading"
- K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
+ K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_subsubsection));
val textP = OuterSyntax.markup_command IsarOutput.MarkupEnv "text" "formal comment (theory)"
- K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text));
+ K.thy_decl (P.text >> (Toplevel.theory o IsarThy.add_text));
val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw"
"raw document preparation text" K.thy_decl
- (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
+ (P.text >> (Toplevel.theory o IsarThy.add_text_raw));
val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
- K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
+ K.prf_heading (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
- K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
+ K.prf_heading (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
"formal comment (proof)" K.prf_heading
- (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
+ (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
- K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
+ K.prf_decl (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw"
"raw document preparation text (proof)" K.prf_decl
- (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
+ (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
@@ -86,53 +86,51 @@
val classesP =
OuterSyntax.command "classes" "declare type classes" K.thy_decl
(Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
- P.!!! (P.list1 P.xname)) [])
- -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
+ P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o Theory.add_classes));
val classrelP =
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
- (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) -- P.marg_comment
- >> (Toplevel.theory o IsarThy.add_classrel));
+ (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
+ >> (Toplevel.theory o Theory.add_classrel o single));
val defaultsortP =
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
- (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));
+ (P.sort >> (Toplevel.theory o Theory.add_defsort));
(* types *)
val typedeclP =
OuterSyntax.command "typedecl" "type declaration" K.thy_decl
- (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
- Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
+ (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
+ Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
val typeabbrP =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
- (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment)
- >> (Toplevel.theory o IsarThy.add_tyabbrs o
- map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
+ (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
+ >> (Toplevel.theory o Theory.add_tyabbrs o
+ map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
val nontermP =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
- K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment)
- >> (Toplevel.theory o IsarThy.add_nonterminals));
+ K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
val aritiesP =
OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
- (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment)
- >> (Toplevel.theory o IsarThy.add_arities));
+ (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
+ >> (Toplevel.theory o Theory.add_arities));
(* consts and syntax *)
val judgmentP =
OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
- (P.const -- P.marg_comment >> (Toplevel.theory o IsarThy.add_judgment));
+ (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
val constsP =
OuterSyntax.command "consts" "declare constants" K.thy_decl
- (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
+ (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
val mode_spec =
@@ -142,8 +140,7 @@
val syntaxP =
OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
- (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment)
- >> (Toplevel.theory o uncurry IsarThy.add_modesyntax));
+ (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
(* translations *)
@@ -162,33 +159,31 @@
val translationsP =
OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
- (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules));
+ (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
(* axioms and definitions *)
val axiomsP =
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
- (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
+ (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
val opt_overloaded =
Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
val defsP =
OuterSyntax.command "defs" "define constants" K.thy_decl
- (opt_overloaded -- Scan.repeat1 (P.spec_name -- P.marg_comment)
- >> (Toplevel.theory o IsarThy.add_defs));
+ (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
val constdefsP =
OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
- (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment))
- >> (Toplevel.theory o IsarThy.add_constdefs));
+ (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o IsarThy.add_constdefs));
(* theorems *)
val in_locale = Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname --| P.$$$ ")"));
-val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1 -- P.marg_comment);
+val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1);
fun theorems kind = in_locale -- name_facts
>> uncurry (#1 ooo IsarThy.smart_theorems kind);
@@ -203,93 +198,92 @@
val declareP =
OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
- (in_locale -- (P.xthms1 -- P.marg_comment)
- >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
+ (in_locale -- P.xthms1 >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
(* name space entry path *)
val globalP =
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
- (P.marg_comment >> (Toplevel.theory o IsarThy.global_path));
+ (Scan.succeed (Toplevel.theory PureThy.global_path));
val localP =
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
- (P.marg_comment >> (Toplevel.theory o IsarThy.local_path));
+ (Scan.succeed (Toplevel.theory PureThy.local_path));
val hideP =
OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
- (P.name -- Scan.repeat1 P.xname -- P.marg_comment >> (Toplevel.theory o IsarThy.hide_space));
+ (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_space));
(* use ML text *)
val useP =
OuterSyntax.command "use" "eval ML text from file" K.diag
- (P.name -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use));
+ (P.name >> (Toplevel.no_timing oo IsarCmd.use));
val mlP =
OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
- (P.text -- P.marg_comment >> IsarCmd.use_mltext true);
+ (P.text >> IsarCmd.use_mltext true);
val ml_commandP =
OuterSyntax.command "ML_command" "eval ML text" K.diag
- (P.text -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
+ (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
val ml_setupP =
OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
- (P.text -- P.marg_comment >> IsarCmd.use_mltext_theory);
+ (P.text >> IsarCmd.use_mltext_theory);
val setupP =
OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
- (P.text -- P.marg_comment >> (Toplevel.theory o IsarCmd.use_setup));
+ (P.text >> (Toplevel.theory o Context.use_setup));
val method_setupP =
OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
- (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2)
- -- P.marg_comment) >> (Toplevel.theory o IsarThy.method_setup));
+ (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
+ >> (Toplevel.theory o IsarThy.method_setup));
(* translation functions *)
val parse_ast_translationP =
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
- (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_ast_translation));
+ (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
val parse_translationP =
OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
- (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_translation));
+ (P.text >> (Toplevel.theory o IsarThy.parse_translation));
val print_translationP =
OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
- (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_translation));
+ (P.text >> (Toplevel.theory o IsarThy.print_translation));
val typed_print_translationP =
OuterSyntax.command "typed_print_translation" "install typed print translation functions"
- K.thy_decl (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.typed_print_translation));
+ K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
val print_ast_translationP =
OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
- (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_ast_translation));
+ (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
val token_translationP =
OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
- (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.token_translation));
+ (P.text >> (Toplevel.theory o IsarThy.token_translation));
(* oracles *)
val oracleP =
OuterSyntax.command "oracle" "install oracle" K.thy_decl
- ((P.name --| P.$$$ "=") -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle));
+ ((P.name --| P.$$$ "=") -- P.text >> (Toplevel.theory o IsarThy.add_oracle));
(* locales *)
val locale_val =
(P.locale_expr --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] ||
- Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty);
+ Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.locale_element)) [] ||
+ Scan.repeat1 P.locale_element >> pair Locale.empty);
val localeP =
OuterSyntax.command "locale" "define named proof context" K.thy_decl
@@ -305,7 +299,7 @@
val in_locale_elems = in_locale --
Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) [];
-val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
+val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
val statement' = P.$$$ "(" |-- statement --| P.!!! (P.$$$ ")") || statement;
fun gen_theorem k =
@@ -337,11 +331,11 @@
(* facts *)
-val facts = P.and_list1 (P.xthms1 -- P.marg_comment);
+val facts = P.and_list1 P.xthms1;
val thenP =
OuterSyntax.command "then" "forward chaining" K.prf_chain
- (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
+ (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.chain)));
val fromP =
OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
@@ -360,7 +354,7 @@
val fixP =
OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
- (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
+ (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
>> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
val assumeP =
@@ -374,19 +368,19 @@
val defP =
OuterSyntax.command "def" "local definition" K.prf_asm
(P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))
- -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
+ >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
val obtainP =
OuterSyntax.command "obtain" "generalized existence"
K.prf_asm_goal
(Scan.optional
- (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
+ (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
--| P.$$$ "where") [] -- statement
>> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
val letP =
OuterSyntax.command "let" "bind text variables" K.prf_decl
- (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
+ (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
>> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
val case_spec =
@@ -395,109 +389,105 @@
val caseP =
OuterSyntax.command "case" "invoke local context" K.prf_asm
- (case_spec -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
+ (case_spec >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
(* proof structure *)
val beginP =
OuterSyntax.command "{" "begin explicit proof block" K.prf_open
- (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block)));
+ (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.begin_block)));
val endP =
OuterSyntax.command "}" "end explicit proof block" K.prf_close
- (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block)));
+ (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.end_block)));
val nextP =
OuterSyntax.command "next" "enter next proof block" K.prf_block
- (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.next_block)));
+ (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.next_block)));
(* end proof *)
val qedP =
OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
- (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed);
+ (Scan.option P.method >> IsarThy.qed);
val terminal_proofP =
OuterSyntax.command "by" "terminal backward proof" K.qed
- (P.method -- P.interest -- Scan.option (P.method -- P.interest)
- -- P.marg_comment >> IsarThy.terminal_proof);
+ (P.method -- Scan.option P.method >> IsarThy.terminal_proof);
val default_proofP =
OuterSyntax.command ".." "default proof" K.qed
- (P.marg_comment >> IsarThy.default_proof);
+ (Scan.succeed IsarThy.default_proof);
val immediate_proofP =
OuterSyntax.command "." "immediate proof" K.qed
- (P.marg_comment >> IsarThy.immediate_proof);
+ (Scan.succeed IsarThy.immediate_proof);
val done_proofP =
OuterSyntax.command "done" "done proof" K.qed
- (P.marg_comment >> IsarThy.done_proof);
+ (Scan.succeed IsarThy.done_proof);
val skip_proofP =
OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
- (P.marg_comment >> IsarThy.skip_proof);
+ (Scan.succeed IsarThy.skip_proof);
val forget_proofP =
OuterSyntax.command "oops" "forget proof" K.qed_global
- (P.marg_comment >> IsarThy.forget_proof);
-
+ (Scan.succeed IsarThy.forget_proof);
(* proof steps *)
val deferP =
OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script
- (Scan.option P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
+ (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
val preferP =
OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script
- (P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
+ (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
val applyP =
OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script
- (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
+ (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
val apply_endP =
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script
- (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
+ (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
val proofP =
OuterSyntax.command "proof" "backward proof" K.prf_block
- (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
- >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
+ (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
(* calculational proof commands *)
val calc_args =
- Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
+ Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")")));
val alsoP =
OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl
- (calc_args -- P.marg_comment >> IsarThy.also);
+ (calc_args >> IsarThy.also);
val finallyP =
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain
- (calc_args -- P.marg_comment >> IsarThy.finally);
+ (calc_args >> IsarThy.finally);
val moreoverP =
OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
- (P.marg_comment >> IsarThy.moreover);
+ (Scan.succeed IsarThy.moreover);
val ultimatelyP =
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
- K.prf_chain (P.marg_comment >> IsarThy.ultimately);
+ K.prf_chain (Scan.succeed IsarThy.ultimately);
(* proof navigation *)
val backP =
OuterSyntax.command "back" "backtracking of proof command" K.prf_script
- (Scan.optional (P.$$$ "!" >> K true) false -- P.marg_comment >>
- (Toplevel.print oo IsarCmd.back));
+ (Scan.optional (P.$$$ "!" >> K true) false >> (Toplevel.print oo IsarCmd.back));
(* history *)
@@ -611,29 +601,27 @@
val print_thmsP =
OuterSyntax.improper_command "thm" "print theorems" K.diag
- (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_thms));
+ (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
val print_prfsP =
OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
- (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >>
- (Toplevel.no_timing oo IsarCmd.print_prfs false));
+ (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
val print_full_prfsP =
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
- (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >>
- (Toplevel.no_timing oo IsarCmd.print_prfs true));
+ (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
val print_propP =
OuterSyntax.improper_command "prop" "read and print proposition" K.diag
- (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prop));
+ (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
val print_termP =
OuterSyntax.improper_command "term" "read and print term" K.diag
- (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_term));
+ (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
val print_typeP =
OuterSyntax.improper_command "typ" "read and print type" K.diag
- (opt_modes -- P.typ -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_type));
+ (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
--- a/src/Pure/Isar/isar_thy.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML Tue Feb 12 20:28:27 2002 +0100
@@ -8,206 +8,154 @@
signature ISAR_THY =
sig
- val add_header: Comment.text -> Toplevel.transition -> Toplevel.transition
- val add_chapter: Comment.text -> theory -> theory
- val add_section: Comment.text -> theory -> theory
- val add_subsection: Comment.text -> theory -> theory
- val add_subsubsection: Comment.text -> theory -> theory
- val add_text: Comment.text -> theory -> theory
- val add_text_raw: Comment.text -> theory -> theory
- val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
- val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
- val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
- val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
- val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T
- val global_path: Comment.text -> theory -> theory
- val local_path: Comment.text -> theory -> theory
- val hide_space: (string * xstring list) * Comment.text -> theory -> theory
- val hide_space_i: (string * string list) * Comment.text -> theory -> theory
- val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
- val add_classes_i: (bclass * class list) list * Comment.text -> theory -> theory
- val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
- val add_classrel_i: (class * class) * Comment.text -> theory -> theory
- val add_defsort: string * Comment.text -> theory -> theory
- val add_defsort_i: sort * Comment.text -> theory -> theory
- val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
- val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
- -> theory -> theory
- val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
- -> theory -> theory
- val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory
- val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
- val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
- val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
- val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list -> theory -> theory
- val add_modesyntax: string * bool -> ((bstring * string * mixfix) * Comment.text) list
- -> theory -> theory
- val add_modesyntax_i: string * bool -> ((bstring * typ * mixfix) * Comment.text) list
- -> theory -> theory
- val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory
- val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory
- val add_judgment: (bstring * string * mixfix) * Comment.text -> theory -> theory
- val add_judgment_i: (bstring * typ * mixfix) * Comment.text -> theory -> theory
- val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
- val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
- -> theory -> theory
- val add_defs: bool * (((bstring * string) * Args.src list) * Comment.text) list
- -> theory -> theory
- val add_defs_i: bool * (((bstring * term) * theory attribute list) * Comment.text) list
- -> theory -> theory
- val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list
- -> theory -> theory
- val add_constdefs_i: (((bstring * typ * mixfix) * Comment.text) * (term * Comment.text)) list
- -> theory -> theory
- val theorems: string ->
- (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+ val add_header: string -> Toplevel.transition -> Toplevel.transition
+ val add_chapter: string -> theory -> theory
+ val add_section: string -> theory -> theory
+ val add_subsection: string -> theory -> theory
+ val add_subsubsection: string -> theory -> theory
+ val add_text: string -> theory -> theory
+ val add_text_raw: string -> theory -> theory
+ val add_sect: string -> ProofHistory.T -> ProofHistory.T
+ val add_subsect: string -> ProofHistory.T -> ProofHistory.T
+ val add_subsubsect: string -> ProofHistory.T -> ProofHistory.T
+ val add_txt: string -> ProofHistory.T -> ProofHistory.T
+ val add_txt_raw: string -> ProofHistory.T -> ProofHistory.T
+ val hide_space: string * xstring list -> theory -> theory
+ val hide_space_i: string * string list -> theory -> theory
+ val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
+ val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
+ val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory
+ val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
+ val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
+ val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
+ val theorems: string -> ((bstring * Args.src list) * (xstring * Args.src list) list) list
-> theory -> theory * (string * thm list) list
val theorems_i: string ->
- (((bstring * theory attribute list)
- * (thm list * theory attribute list) list) * Comment.text) list
+ ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
-> theory -> theory * (string * thm list) list
val locale_theorems: string -> xstring ->
- (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+ ((bstring * Args.src list) * (xstring * Args.src list) list) list
-> theory -> theory * (bstring * thm list) list
val locale_theorems_i: string -> string ->
- (((bstring * Proof.context attribute list)
- * (thm list * Proof.context attribute list) list) * Comment.text) list
+ ((bstring * Proof.context attribute list)
+ * (thm list * Proof.context attribute list) list) list
-> theory -> theory * (string * thm list) list
val smart_theorems: string -> xstring option ->
- (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+ ((bstring * Args.src list) * (xstring * Args.src list) list) list
-> theory -> theory * (string * thm list) list
- val declare_theorems: xstring option -> (xstring * Args.src list) list * Comment.text
- -> theory -> theory
+ val declare_theorems: xstring option -> (xstring * Args.src list) list -> theory -> theory
val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
- val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list
- -> ProofHistory.T -> ProofHistory.T
- val have_facts_i: (((string * Proof.context attribute list) *
- (thm * Proof.context attribute list) list) * Comment.text) list
+ val have_facts: ((string * Args.src list) * (string * Args.src list) list) list
-> ProofHistory.T -> ProofHistory.T
- val from_facts: ((string * Args.src list) list * Comment.text) list
- -> ProofHistory.T -> ProofHistory.T
- val from_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list
+ val have_facts_i: ((string * Proof.context attribute list) *
+ (thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T
+ val from_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+ val from_facts_i: (thm * Proof.context attribute list) list list
-> ProofHistory.T -> ProofHistory.T
- val with_facts: ((string * Args.src list) list * Comment.text) list
- -> ProofHistory.T -> ProofHistory.T
- val with_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list
+ val with_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+ val with_facts_i: (thm * Proof.context attribute list) list list
-> ProofHistory.T -> ProofHistory.T
- val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
- val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val let_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val let_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val invoke_case: (string * string option list * Args.src list) * Comment.text
+ val chain: ProofHistory.T -> ProofHistory.T
+ val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
+ val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
+ val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
+ val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
+ val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T
+ val invoke_case_i: string * string option list * Proof.context attribute list
-> ProofHistory.T -> ProofHistory.T
- val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text
- -> ProofHistory.T -> ProofHistory.T
- val theorem: string
- -> ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text
+ val theorem: string -> (bstring * Args.src list) * (string * (string list * string list))
-> bool -> theory -> ProofHistory.T
- val theorem_i: string -> ((bstring * theory attribute list) *
- (term * (term list * term list))) * Comment.text -> bool -> theory -> ProofHistory.T
+ val theorem_i: string -> (bstring * theory attribute list) *
+ (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
val multi_theorem: string -> bstring * Args.src list ->
Args.src Locale.element list ->
- (((bstring * Args.src list) * (string * (string list * string list)) list)
- * Comment.text) list -> bool -> theory -> ProofHistory.T
+ ((bstring * Args.src list) * (string * (string list * string list)) list) list
+ -> bool -> theory -> ProofHistory.T
val multi_theorem_i: string -> bstring * theory attribute list ->
Proof.context attribute Locale.element_i list ->
- (((bstring * theory attribute list) * (term * (term list * term list)) list)
- * Comment.text) list -> bool -> theory -> ProofHistory.T
+ ((bstring * theory attribute list) * (term * (term list * term list)) list) list
+ -> bool -> theory -> ProofHistory.T
val locale_multi_theorem: string -> bstring * Args.src list ->
xstring -> Args.src Locale.element list ->
- (((bstring * Args.src list) * (string * (string list * string list)) list)
- * Comment.text) list -> bool -> theory -> ProofHistory.T
+ ((bstring * Args.src list) * (string * (string list * string list)) list) list
+ -> bool -> theory -> ProofHistory.T
val locale_multi_theorem_i: string -> bstring * theory attribute list ->
string -> Proof.context attribute Locale.element_i list ->
- (((bstring * Proof.context attribute list) * (term * (term list * term list)) list)
- * Comment.text) list -> bool -> theory -> ProofHistory.T
+ ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
+ -> bool -> theory -> ProofHistory.T
val smart_multi_theorem: string -> bstring * Args.src list ->
xstring Library.option * Args.src Locale.element list ->
- (((bstring * Args.src list) * (string * (string list * string list)) list)
- * Comment.text) list -> bool -> theory -> ProofHistory.T
- val assume: (((string * Args.src list) * (string * (string list * string list)) list)
- * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val assume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list)
- * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val presume: (((string * Args.src list) * (string * (string list * string list)) list)
- * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val presume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list)
- * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val have: (((string * Args.src list) *
- (string * (string list * string list)) list) * Comment.text) list
+ ((bstring * Args.src list) * (string * (string list * string list)) list) list
+ -> bool -> theory -> ProofHistory.T
+ val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val have_i: (((string * Proof.context attribute list) *
- (term * (term list * term list)) list) * Comment.text) list
+ val assume_i:
+ ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
+ -> ProofHistory.T -> ProofHistory.T
+ val presume: ((string * Args.src list) * (string * (string list * string list)) list) list
+ -> ProofHistory.T -> ProofHistory.T
+ val presume_i:
+ ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val hence: (((string * Args.src list) *
- (string * (string list * string list)) list) * Comment.text) list
+ val have: ((string * Args.src list) * (string * (string list * string list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val hence_i: (((string * Proof.context attribute list) *
- (term * (term list * term list)) list) * Comment.text) list
+ val have_i: ((string * Proof.context attribute list) *
+ (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
+ val hence: ((string * Args.src list) * (string * (string list * string list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val show: (((string * Args.src list) *
- (string * (string list * string list)) list) * Comment.text) list
+ val hence_i: ((string * Proof.context attribute list) *
+ (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
+ val show: ((string * Args.src list) * (string * (string list * string list)) list) list
-> bool -> ProofHistory.T -> ProofHistory.T
- val show_i: (((string * Proof.context attribute list) *
- (term * (term list * term list)) list) * Comment.text) list
- -> bool -> ProofHistory.T -> ProofHistory.T
- val thus: (((string * Args.src list) *
- (string * (string list * string list)) list) * Comment.text) list
- -> bool -> ProofHistory.T -> ProofHistory.T
- val thus_i: (((string * Proof.context attribute list) *
- (term * (term list * term list)) list) * Comment.text) list
+ val show_i: ((string * Proof.context attribute list) *
+ (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
+ val thus: ((string * Args.src list) * (string * (string list * string list)) list) list
-> bool -> ProofHistory.T -> ProofHistory.T
- val local_def: ((string * Args.src list) * (string * (string * string list)))
- * Comment.text -> ProofHistory.T -> ProofHistory.T
- val local_def_i: ((string * Args.src list) * (string * (term * term list)))
- * Comment.text -> ProofHistory.T -> ProofHistory.T
- val obtain: ((string list * string option) * Comment.text) list
- * (((string * Args.src list) * (string * (string list * string list)) list)
- * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val obtain_i: ((string list * typ option) * Comment.text) list
- * (((string * Proof.context attribute list) * (term * (term list * term list)) list)
- * Comment.text) list -> ProofHistory.T -> ProofHistory.T
- val begin_block: Comment.text -> ProofHistory.T -> ProofHistory.T
- val next_block: Comment.text -> ProofHistory.T -> ProofHistory.T
- val end_block: Comment.text -> ProofHistory.T -> ProofHistory.T
- val defer: int option * Comment.text -> ProofHistory.T -> ProofHistory.T
- val prefer: int * Comment.text -> ProofHistory.T -> ProofHistory.T
- val apply: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
- val apply_end: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
- val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
+ val thus_i: ((string * Proof.context attribute list)
+ * (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
+ val local_def: (string * Args.src list) * (string * (string * string list))
+ -> ProofHistory.T -> ProofHistory.T
+ val local_def_i: (string * Args.src list) * (string * (term * term list))
+ -> ProofHistory.T -> ProofHistory.T
+ val obtain: (string list * string option) list
+ * ((string * Args.src list) * (string * (string list * string list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val qed: (Method.text * Comment.interest) option * Comment.text
+ val obtain_i: (string list * typ option) list
+ * ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
+ -> ProofHistory.T -> ProofHistory.T
+ val begin_block: ProofHistory.T -> ProofHistory.T
+ val next_block: ProofHistory.T -> ProofHistory.T
+ val end_block: ProofHistory.T -> ProofHistory.T
+ val defer: int option -> ProofHistory.T -> ProofHistory.T
+ val prefer: int -> ProofHistory.T -> ProofHistory.T
+ val apply: Method.text -> ProofHistory.T -> ProofHistory.T
+ val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
+ val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
+ val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
+ val terminal_proof: Method.text * Method.text option
-> Toplevel.transition -> Toplevel.transition
- val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
- * Comment.text -> Toplevel.transition -> Toplevel.transition
- val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
- val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
- val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
- val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
- val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
+ val default_proof: Toplevel.transition -> Toplevel.transition
+ val immediate_proof: Toplevel.transition -> Toplevel.transition
+ val done_proof: Toplevel.transition -> Toplevel.transition
+ val skip_proof: Toplevel.transition -> Toplevel.transition
+ val forget_proof: Toplevel.transition -> Toplevel.transition
val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
- val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
- -> Toplevel.transition -> Toplevel.transition
- val also_i: (thm list * Comment.interest) option * Comment.text
- -> Toplevel.transition -> Toplevel.transition
- val finally: ((string * Args.src list) list * Comment.interest) option * Comment.text
- -> Toplevel.transition -> Toplevel.transition
- val finally_i: (thm list * Comment.interest) option * Comment.text
- -> Toplevel.transition -> Toplevel.transition
- val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
- val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition
- val parse_ast_translation: string * Comment.text -> theory -> theory
- val parse_translation: string * Comment.text -> theory -> theory
- val print_translation: string * Comment.text -> theory -> theory
- val typed_print_translation: string * Comment.text -> theory -> theory
- val print_ast_translation: string * Comment.text -> theory -> theory
- val token_translation: string * Comment.text -> theory -> theory
- val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
- val add_oracle: (bstring * string) * Comment.text -> theory -> theory
- val add_locale: bstring * Locale.expr * (Args.src Locale.element * Comment.text) list
- -> theory -> theory
+ val also: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+ val also_i: thm list option -> Toplevel.transition -> Toplevel.transition
+ val finally: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+ val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition
+ val moreover: Toplevel.transition -> Toplevel.transition
+ val ultimately: Toplevel.transition -> Toplevel.transition
+ val parse_ast_translation: string -> theory -> theory
+ val parse_translation: string -> theory -> theory
+ val print_translation: string -> theory -> theory
+ val typed_print_translation: string -> theory -> theory
+ val print_ast_translation: string -> theory -> theory
+ val token_translation: string -> theory -> theory
+ val method_setup: bstring * string * string -> theory -> theory
+ val add_oracle: bstring * string -> theory -> theory
+ val add_locale: bstring * Locale.expr * Args.src Locale.element list -> theory -> theory
val begin_theory: string -> string list -> (string * bool) list -> theory
val end_theory: theory -> theory
val kill_theory: string -> unit
@@ -225,21 +173,20 @@
(* markup commands *)
-fun add_header comment =
+fun add_header x =
Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
fun add_text _ x = x;
fun add_text_raw _ x = x;
-fun add_heading add present txt thy =
- (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy);
+fun add_heading add present txt thy = (Context.setmp (Some thy) present txt; add txt thy);
val add_chapter = add_heading add_text Present.section;
val add_section = add_heading add_text Present.section;
val add_subsection = add_heading add_text Present.subsection;
val add_subsubsection = add_heading add_text Present.subsubsection;
-fun add_txt (_: Comment.text) = ProofHistory.apply I;
+fun add_txt (_: string) = ProofHistory.apply I;
val add_txt_raw = add_txt;
val add_sect = add_txt;
val add_subsect = add_txt;
@@ -248,9 +195,6 @@
(* name spaces *)
-fun global_path comment_ignore = PureThy.global_path;
-fun local_path comment_ignore = PureThy.local_path;
-
local
val kinds =
@@ -259,7 +203,7 @@
can (Sign.certify_tycon sg) c orelse can (Sign.certify_tyabbr sg) c),
(Sign.constK, can o Sign.certify_const)];
-fun gen_hide intern ((kind, xnames), comment_ignore) thy =
+fun gen_hide intern (kind, xnames) thy =
(case assoc (kinds, kind) of
Some check =>
let
@@ -280,51 +224,27 @@
end;
-(* signature and syntax *)
-
-val add_classes = Theory.add_classes o Comment.ignore;
-val add_classes_i = Theory.add_classes_i o Comment.ignore;
-val add_classrel = Theory.add_classrel o single o Comment.ignore;
-val add_classrel_i = Theory.add_classrel_i o single o Comment.ignore;
-val add_defsort = Theory.add_defsort o Comment.ignore;
-val add_defsort_i = Theory.add_defsort_i o Comment.ignore;
-val add_nonterminals = Theory.add_nonterminals o map Comment.ignore;
-val add_tyabbrs = Theory.add_tyabbrs o map Comment.ignore;
-val add_tyabbrs_i = Theory.add_tyabbrs_i o map Comment.ignore;
-val add_arities = Theory.add_arities o map Comment.ignore;
-val add_arities_i = Theory.add_arities_i o map Comment.ignore;
-val add_typedecl = PureThy.add_typedecls o single o Comment.ignore;
-val add_consts = Theory.add_consts o map Comment.ignore;
-val add_consts_i = Theory.add_consts_i o map Comment.ignore;
-fun add_modesyntax mode = Theory.add_modesyntax mode o map Comment.ignore;
-fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
-val add_trrules = Theory.add_trrules o map Comment.ignore;
-val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
-val add_judgment = ObjectLogic.add_judgment o Comment.ignore;
-val add_judgment_i = ObjectLogic.add_judgment_i o Comment.ignore;
-
-
(* axioms and defs *)
fun add_axms f args thy =
f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
-val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
-val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
-fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) (map Comment.ignore args);
-fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) (map Comment.ignore args);
+val add_axioms = add_axms (#1 oo PureThy.add_axioms);
+val add_axioms_i = #1 oo PureThy.add_axioms_i;
+fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args;
+fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args;
(* constdefs *)
fun gen_add_constdefs consts defs args thy =
thy
- |> consts (map (Comment.ignore o fst) args)
- |> defs (false, map (fn (((c, _, mx), _), (s, _)) =>
- (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
+ |> consts (map fst args)
+ |> defs (false, map (fn ((c, _, mx), s) =>
+ ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
-fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args;
-fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args;
+val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;
+val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;
(* attributes *)
@@ -355,30 +275,27 @@
in
-fun theorems_i k = (present_thmss k oo PureThy.have_thmss_i (Drule.kind k)) o map Comment.ignore;
-fun locale_theorems_i k loc = (present_thmss k oo Locale.have_thmss_i k loc) o map Comment.ignore;
+fun theorems_i k = present_thmss k oo PureThy.have_thmss_i (Drule.kind k);
+fun locale_theorems_i k loc = present_thmss k oo Locale.have_thmss_i k loc;
fun theorems k args thy = thy
- |> PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args))
+ |> PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
|> present_thmss k;
fun locale_theorems k loc args thy = thy
- |> Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args))
+ |> Locale.have_thmss k loc (local_attribs thy args)
|> present_thmss k;
fun smart_theorems k opt_loc args thy = thy
|> (case opt_loc of
- None => PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args))
- | Some loc => Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args)))
+ None => PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
+ | Some loc => Locale.have_thmss k loc (local_attribs thy args))
|> present_thmss k;
-fun declare_theorems opt_loc (args, comment) =
- #1 o smart_theorems "" opt_loc [((("", []), args), comment)];
+fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
-fun apply_theorems args =
- apsnd (flat o map snd) o theorems "" [((("", []), args), Comment.none)];
-fun apply_theorems_i args =
- apsnd (flat o map snd) o theorems_i "" [((("", []), args), Comment.none)];
+fun apply_theorems args = apsnd (flat o map snd) o theorems "" [(("", []), args)];
+fun apply_theorems_i args = apsnd (flat o map snd) o theorems_i "" [(("", []), args)];
end;
@@ -391,25 +308,25 @@
fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
-val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss o map Comment.ignore;
-val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i o map Comment.ignore;
-val from_facts = chain_thmss (local_thmss Proof.have_thmss) o map Comment.ignore;
-val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i) o map Comment.ignore;
-val with_facts = chain_thmss (local_thmss Proof.with_thmss) o map Comment.ignore;
-val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i) o map Comment.ignore;
-fun chain comment_ignore = ProofHistory.apply Proof.chain;
+val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss;
+val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i;
+val from_facts = chain_thmss (local_thmss Proof.have_thmss);
+val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i);
+val with_facts = chain_thmss (local_thmss Proof.with_thmss);
+val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i);
+val chain = ProofHistory.apply Proof.chain;
(* context *)
-val fix = ProofHistory.apply o Proof.fix o map Comment.ignore;
-val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
-val let_bind = ProofHistory.apply o Proof.let_bind o map Comment.ignore;
-val let_bind_i = ProofHistory.apply o Proof.let_bind_i o map Comment.ignore;
+val fix = ProofHistory.apply o Proof.fix;
+val fix_i = ProofHistory.apply o Proof.fix_i;
+val let_bind = ProofHistory.apply o Proof.let_bind;
+val let_bind_i = ProofHistory.apply o Proof.let_bind_i;
-fun invoke_case ((name, xs, src), comment_ignore) = ProofHistory.apply (fn state =>
+fun invoke_case (name, xs, src) = ProofHistory.apply (fn state =>
Proof.invoke_case (name, xs, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
-val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
+val invoke_case_i = ProofHistory.apply o Proof.invoke_case;
(* local results *)
@@ -487,94 +404,80 @@
fun multi_theorem k a elems args int thy =
global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a) None
- (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy;
+ (map (Locale.attribute (Attrib.local_attribute thy)) elems)) args int thy;
-fun multi_theorem_i k a elems =
- global_statement_i (Proof.multi_theorem_i k a None elems) o map Comment.ignore;
+fun multi_theorem_i k a elems = global_statement_i (Proof.multi_theorem_i k a None elems);
fun locale_multi_theorem k a locale elems args int thy =
global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a)
- (Some (locale, map (map (Attrib.local_attribute thy) o snd o fst o Comment.ignore) args))
+ (Some (locale, map (map (Attrib.local_attribute thy) o snd o fst) args))
(map (Locale.attribute (Attrib.local_attribute thy)) elems))
- (map (apfst (apsnd (K [])) o Comment.ignore) args) int thy;
+ (map (apfst (apsnd (K []))) args) int thy;
fun locale_multi_theorem_i k a locale elems args =
- global_statement_i (Proof.multi_theorem_i k a
- (Some (locale, map (snd o fst o Comment.ignore) args)) elems)
- (map (apfst (apsnd (K [])) o Comment.ignore) args);
+ global_statement_i (Proof.multi_theorem_i k a (Some (locale, map (snd o fst) args)) elems)
+ (map (apfst (apsnd (K []))) args);
-fun theorem k ((a, t), cmt) = multi_theorem k a [] [((("", []), [t]), cmt)];
-fun theorem_i k ((a, t), cmt) = multi_theorem_i k a [] [((("", []), [t]), cmt)];
+fun theorem k (a, t) = multi_theorem k a [] [(("", []), [t])];
+fun theorem_i k (a, t) = multi_theorem_i k a [] [(("", []), [t])];
fun smart_multi_theorem k a (None, elems) = multi_theorem k a elems
| smart_multi_theorem k a (Some locale, elems) = locale_multi_theorem k a locale elems;
-val assume = local_statement Proof.assume I o map Comment.ignore;
-val assume_i = local_statement_i Proof.assume_i I o map Comment.ignore;
-val presume = local_statement Proof.presume I o map Comment.ignore;
-val presume_i = local_statement_i Proof.presume_i I o map Comment.ignore;
-val have = local_statement (Proof.have Seq.single) I o map Comment.ignore;
-val have_i = local_statement_i (Proof.have_i Seq.single) I o map Comment.ignore;
-val hence = local_statement (Proof.have Seq.single) Proof.chain o map Comment.ignore;
-val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o map Comment.ignore;
-val show = local_statement' (Proof.show check_goal Seq.single) I o map Comment.ignore;
-val show_i = local_statement_i' (Proof.show_i check_goal Seq.single) I o map Comment.ignore;
-val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain o map Comment.ignore;
-val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain o map Comment.ignore;
+val assume = local_statement Proof.assume I;
+val assume_i = local_statement_i Proof.assume_i I;
+val presume = local_statement Proof.presume I;
+val presume_i = local_statement_i Proof.presume_i I;
+val have = local_statement (Proof.have Seq.single) I;
+val have_i = local_statement_i (Proof.have_i Seq.single) I;
+val hence = local_statement (Proof.have Seq.single) Proof.chain;
+val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain;
+val show = local_statement' (Proof.show check_goal Seq.single) I;
+val show_i = local_statement_i' (Proof.show_i check_goal Seq.single) I;
+val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain;
+val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain;
fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state =>
f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state);
-val local_def = gen_def Proof.def o Comment.ignore;
-val local_def_i = gen_def Proof.def_i o Comment.ignore;
+val local_def = gen_def Proof.def;
+val local_def_i = gen_def Proof.def_i;
fun obtain (xs, asms) = ProofHistory.applys (fn state =>
- Obtain.obtain (map Comment.ignore xs)
- (map (local_attributes' state) (map Comment.ignore asms)) state);
+ Obtain.obtain xs (map (local_attributes' state) asms) state);
-fun obtain_i (xs, asms) = ProofHistory.applys (fn state =>
- Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms) state);
+fun obtain_i (xs, asms) = ProofHistory.applys (Obtain.obtain_i xs asms);
end;
(* blocks *)
-fun begin_block comment_ignore = ProofHistory.apply Proof.begin_block;
-fun next_block comment_ignore = ProofHistory.apply Proof.next_block;
-fun end_block comment_ignore = ProofHistory.applys Proof.end_block;
+val begin_block = ProofHistory.apply Proof.begin_block;
+val next_block = ProofHistory.apply Proof.next_block;
+val end_block = ProofHistory.applys Proof.end_block;
(* shuffle state *)
fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
-fun defer (i, comment_ignore) = ProofHistory.applys (shuffle Method.defer i);
-fun prefer (i, comment_ignore) = ProofHistory.applys (shuffle Method.prefer i);
+fun defer i = ProofHistory.applys (shuffle Method.defer i);
+fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
(* backward steps *)
-fun apply (m, comment_ignore) = ProofHistory.applys
+fun apply m = ProofHistory.applys
(Seq.map (Proof.goal_facts (K [])) o Method.refine m o Proof.assert_backward);
-
-fun apply_end (m, comment_ignore) = ProofHistory.applys
- (Method.refine_end m o Proof.assert_forward);
-
-val proof = ProofHistory.applys o Method.proof o
- apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;
+fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
+val proof = ProofHistory.applys o Method.proof;
(* local endings *)
-val local_qed =
- proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest;
-
-fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
-
-val local_terminal_proof =
- proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
-
+val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true);
+val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof);
val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
@@ -596,9 +499,8 @@
thy
end);
-fun global_qed m = global_result (K (Method.global_qed true (apsome Comment.ignore_interest m)));
-fun global_terminal_proof m =
- global_result (K (Method.global_terminal_proof (ignore_interests m)));
+fun global_qed m = global_result (K (Method.global_qed true m));
+fun global_terminal_proof m = global_result (K (Method.global_terminal_proof m));
val global_default_proof = global_result (K Method.global_default_proof);
val global_immediate_proof = global_result (K Method.global_immediate_proof);
val global_skip_proof = global_result SkipProof.global_skip_proof;
@@ -607,14 +509,13 @@
(* common endings *)
-fun qed (meth, comment) = local_qed meth o global_qed meth;
-fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
-fun default_proof comment = local_default_proof o global_default_proof;
-fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
-fun done_proof comment = local_done_proof o global_done_proof;
-fun skip_proof comment = local_skip_proof o global_skip_proof;
-
-fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
+fun qed meth = local_qed meth o global_qed meth;
+fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
+val default_proof = local_default_proof o global_default_proof;
+val immediate_proof = local_immediate_proof o global_immediate_proof;
+val done_proof = local_done_proof o global_done_proof;
+val skip_proof = local_skip_proof o global_skip_proof;
+val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
(* calculational proof commands *)
@@ -628,8 +529,8 @@
fun proof''' f = Toplevel.proof' (f o cond_print_calc);
-fun gen_calc get f (args, _) prt state =
- f (apsome (fn (srcs, _) => get srcs state) args) prt state;
+fun gen_calc get f args prt state =
+ f (apsome (fn srcs => get srcs state) args) prt state;
in
@@ -640,8 +541,8 @@
fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
-fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
-fun ultimately comment = proof''' (ProofHistory.apply o Calculation.ultimately);
+val moreover = proof''' (ProofHistory.apply o Calculation.moreover);
+val ultimately = proof''' (ProofHistory.apply o Calculation.ultimately);
end;
@@ -650,32 +551,32 @@
val parse_ast_translation =
Context.use_let "val parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
- "Theory.add_trfuns (parse_ast_translation, [], [], [])" o Comment.ignore;
+ "Theory.add_trfuns (parse_ast_translation, [], [], [])";
val parse_translation =
Context.use_let "val parse_translation: (string * (term list -> term)) list"
- "Theory.add_trfuns ([], parse_translation, [], [])" o Comment.ignore;
+ "Theory.add_trfuns ([], parse_translation, [], [])";
val print_translation =
Context.use_let "val print_translation: (string * (term list -> term)) list"
- "Theory.add_trfuns ([], [], print_translation, [])" o Comment.ignore;
+ "Theory.add_trfuns ([], [], print_translation, [])";
val print_ast_translation =
Context.use_let "val print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
- "Theory.add_trfuns ([], [], [], print_ast_translation)" o Comment.ignore;
+ "Theory.add_trfuns ([], [], [], print_ast_translation)";
val typed_print_translation =
Context.use_let "val typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
- "Theory.add_trfunsT typed_print_translation" o Comment.ignore;
+ "Theory.add_trfunsT typed_print_translation";
val token_translation =
Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
- "Theory.add_tokentrfuns token_translation" o Comment.ignore;
+ "Theory.add_tokentrfuns token_translation";
(* add method *)
-fun method_setup ((name, txt, cmt), comment_ignore) =
+fun method_setup (name, txt, cmt) =
Context.use_let
"val thm = PureThy.get_thm_closure (Context.the_context ());\n\
\val thms = PureThy.get_thms_closure (Context.the_context ());\n\
@@ -686,7 +587,7 @@
(* add_oracle *)
-fun add_oracle ((name, txt), comment_ignore) =
+fun add_oracle (name, txt) =
Context.use_let
"val oracle: bstring * (Sign.sg * Object.T -> term)"
"Theory.add_oracle oracle"
@@ -696,8 +597,7 @@
(* add_locale *)
fun add_locale (name, import, body) thy =
- Locale.add_locale name import
- (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body) thy;
+ Locale.add_locale name import (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
(* theory init and exit *)
--- a/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:28:27 2002 +0100
@@ -45,9 +45,6 @@
val xname: token list -> xstring * token list
val text: token list -> string * token list
val uname: token list -> string option * token list
- val comment: token list -> Comment.text * token list
- val marg_comment: token list -> Comment.text * token list
- val interest: token list -> Comment.interest * token list
val sort: token list -> string * token list
val arity: token list -> (string list * string) * token list
val simple_arity: token list -> (string list * xclass) * token list
@@ -177,15 +174,6 @@
val uname = underscore >> K None || name >> Some;
-(* formal comments *)
-
-val comment = text >> (Comment.plain o Library.single);
-val marg_comment = Scan.repeat ($$$ "--" |-- text) >> Comment.plain;
-
-val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
- $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;
-
-
(* sorts and arities *)
val sort = group "sort" xname;
--- a/src/Pure/Isar/outer_syntax.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Tue Feb 12 20:28:27 2002 +0100
@@ -228,20 +228,19 @@
(* basic sources *)
-fun token_source (src, pos) =
- src
- |> Symbol.source false
- |> T.source false (K (get_lexicons ())) pos;
-
fun toplevel_source term do_recover cmd src =
let
val no_terminator =
Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
- val recover = Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None];
+ fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]) x;
in
src
+ |> T.source_proper
|> Source.source T.stopper
- (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
+ (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some))
+ (if do_recover then Some recover else None)
+ |> Source.mapfilter I
+ |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
(if do_recover then Some recover else None)
|> Source.mapfilter I
end;
@@ -254,7 +253,6 @@
|> Symbol.source true
|> T.source true get_lexicons
(if no_pos then Position.none else Position.line_name 1 "stdin")
- |> T.source_proper
|> toplevel_source term true get_parser;
@@ -294,7 +292,6 @@
fun parse_thy src =
src
- |> T.source_proper
|> toplevel_source false false (K (get_parser ()))
|> Source.exhaust;
@@ -311,7 +308,10 @@
Present.old_symbol_source name present_text) (*note: text presented twice*)
else
let
- val tok_src = Source.exhausted (token_source (text_src, pos));
+ val tok_src = text_src
+ |> Symbol.source false
+ |> T.source false (K (get_lexicons ())) pos
+ |> Source.exhausted;
val out = Toplevel.excursion_result
(IsarOutput.parse_thy markup (#1 (get_lexicons ()))
(parse_thy tok_src) tok_src);
--- a/src/Pure/axclass.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/axclass.ML Tue Feb 12 20:28:27 2002 +0100
@@ -26,12 +26,10 @@
val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
val default_intro_classes_tac: thm list -> int -> tactic
val axclass_tac: thm list -> tactic
- val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
- val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
- val instance_arity_proof: (xstring * string list * xclass) * Comment.text
- -> bool -> theory -> ProofHistory.T
- val instance_arity_proof_i: (string * sort list * class) * Comment.text
- -> bool -> theory -> ProofHistory.T
+ val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
+ val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
+ val instance_arity_proof: xstring * string list * xclass -> bool -> theory -> ProofHistory.T
+ val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
val setup: (theory -> theory) list
end;
@@ -421,10 +419,10 @@
fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
-fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
+fun inst_proof mk_prop add_thms sig_prop int thy =
thy
- |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
- (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
+ |> IsarThy.theorem_i Drule.internalK (("", [inst_attribute add_thms]),
+ (mk_prop (Theory.sign_of thy) sig_prop, ([], []))) int;
val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
@@ -448,17 +446,14 @@
val axclassP =
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
- (((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
- P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
- -- Scan.repeat (P.spec_name --| P.marg_comment)
+ ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+ P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
>> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
val instanceP =
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
- ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname)
- -- P.marg_comment >> instance_subclass_proof ||
- (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment
- >> instance_arity_proof)
+ ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof ||
+ (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) >> instance_arity_proof)
>> (Toplevel.print oo Toplevel.theory_to_proof));
val _ = OuterSyntax.add_parsers [axclassP, instanceP];
--- a/src/ZF/Tools/datatype_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/ZF/Tools/datatype_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -419,14 +419,14 @@
val con_decl =
P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
- --| P.marg_comment >> P.triple1;
+ >> P.triple1;
val datatype_decl =
- (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term --| P.marg_comment) "") --
+ (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
- Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
+ Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
+ Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
+ Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
>> (Toplevel.theory o mk_datatype);
val coind_prefix = if coind then "co" else "";
--- a/src/ZF/Tools/ind_cases.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/ZF/Tools/ind_cases.ML Tue Feb 12 20:28:27 2002 +0100
@@ -55,8 +55,8 @@
val read_prop = ProofContext.read_prop (ProofContext.init thy);
val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
val facts = args |> map (fn ((name, srcs), props) =>
- (((name, map (Attrib.global_attribute thy) srcs),
- map (Thm.no_attributes o single o mk_cases) props), Comment.none));
+ ((name, map (Attrib.global_attribute thy) srcs),
+ map (Thm.no_attributes o single o mk_cases) props));
in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
@@ -84,7 +84,7 @@
local structure P = OuterParse and K = OuterSyntax.Keyword in
val ind_cases =
- P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment)
+ P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
>> (Toplevel.theory o inductive_cases);
val inductive_casesP =
--- a/src/ZF/Tools/inductive_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -605,13 +605,13 @@
val ind_decl =
(P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
- ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term)) --| P.marg_comment) --
+ ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) --
(P.$$$ "intros" |--
- P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
- Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
- Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
+ P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
+ Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
+ Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] --
+ Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
+ Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
>> (Toplevel.theory o mk_ind);
val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
--- a/src/ZF/Tools/primrec_package.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/ZF/Tools/primrec_package.ML Tue Feb 12 20:28:27 2002 +0100
@@ -202,7 +202,7 @@
local structure P = OuterParse and K = OuterSyntax.Keyword in
-val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
+val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
val primrecP =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl