# HG changeset patch # User wenzelm # Date 927656650 -7200 # Node ID b6e167580a32ed3c787619417f8085d613ec99ef # Parent b51b25db7bc67bb019a13374d01d65f72388ec9c formal comments (still dummy); diff -r b51b25db7bc6 -r b6e167580a32 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue May 25 20:24:10 1999 +0200 @@ -670,7 +670,7 @@ 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.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment)); fun mk_datatype args = let diff -r b51b25db7bc6 -r b6e167580a32 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/inductive_package.ML Tue May 25 20:24:10 1999 +0200 @@ -710,10 +710,11 @@ #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; fun ind_decl coind = - Scan.repeat1 P.term -- - (P.$$$ "intrs" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term))) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- - Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] + (Scan.repeat1 P.term --| P.marg_comment) -- + (P.$$$ "intrs" |-- + P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment))) -- + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- + Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] >> (Toplevel.theory o mk_ind coind); val inductiveP = diff -r b51b25db7bc6 -r b6e167580a32 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/primrec_package.ML Tue May 25 20:24:10 1999 +0200 @@ -265,7 +265,7 @@ val primrec_decl = Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- - Scan.repeat1 (P.opt_thm_name ":" -- P.term); + Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment); val primrecP = OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl diff -r b51b25db7bc6 -r b6e167580a32 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/recdef_package.ML Tue May 25 20:24:10 1999 +0200 @@ -139,7 +139,7 @@ local structure P = OuterParse and K = OuterSyntax.Keyword in val recdef_decl = - P.name -- P.term -- Scan.repeat1 P.term -- + P.name -- P.term -- Scan.repeat1 (P.term --| P.marg_comment) -- Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] -- Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")")) >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs); diff -r b51b25db7bc6 -r b6e167580a32 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/record_package.ML Tue May 25 20:24:10 1999 +0200 @@ -882,7 +882,7 @@ val record_decl = P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") - -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ))); + -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ) --| P.marg_comment)); val recordP = OuterSyntax.command "record" "define extensible record" K.thy_decl diff -r b51b25db7bc6 -r b6e167580a32 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/typedef_package.ML Tue May 25 20:24:10 1999 +0200 @@ -15,9 +15,9 @@ term -> string list -> thm list -> tactic option -> theory -> theory val add_typedef_i_no_def: string -> bstring * string list * mixfix -> term -> string list -> thm list -> tactic option -> theory -> theory - val typedef_proof: string -> bstring * string list * mixfix -> string + val typedef_proof: (string * (bstring * string list * mixfix) * string) * Comment.text -> bool -> theory -> ProofHistory.T - val typedef_proof_i: string -> bstring * string list * mixfix -> term + val typedef_proof_i: (string * (bstring * string list * mixfix) * term) * Comment.text -> bool -> theory -> ProofHistory.T end; @@ -189,13 +189,13 @@ fun typedef_attribute cset do_typedef (thy, thm) = (check_nonempty cset thm; (thy |> do_typedef, thm)); -fun gen_typedef_proof prep_term name typ set int thy = +fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy = let val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy; val goal = Thm.term_of (goal_nonempty cset); in thy - |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) int + |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int end; val typedef_proof = gen_typedef_proof read_term; @@ -209,16 +209,16 @@ val typedeclP = OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl - (P.type_args -- P.name -- P.opt_mixfix >> (fn ((vs, t), mx) => + (P.type_args -- P.name -- P.opt_mixfix --| P.marg_comment >> (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); + (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- P.marg_comment; -fun mk_typedef_proof (((opt_name, (vs, t)), mx), A) = - typedef_proof (if_none opt_name (Syntax.type_name t mx)) (t, vs, mx) A; +fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), comment) = + typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A), comment); val typedefP = OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal diff -r b51b25db7bc6 -r b6e167580a32 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/Pure/axclass.ML Tue May 25 20:24:10 1999 +0200 @@ -30,10 +30,12 @@ -> tactic option -> thm val goal_subclass: theory -> xclass * xclass -> thm list val goal_arity: theory -> xstring * xsort list * xclass -> thm list - 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 * xsort list * xclass -> bool -> theory -> ProofHistory.T - val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T + 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 * xsort list * xclass) * Comment.text + -> bool -> theory -> ProofHistory.T + val instance_arity_proof_i: (string * sort list * class) * Comment.text + -> bool -> theory -> ProofHistory.T val setup: (theory -> theory) list end; @@ -403,10 +405,10 @@ fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm); -fun inst_proof mk_prop add_thms sig_prop int thy = +fun inst_proof mk_prop add_thms (sig_prop, comment) int thy = thy - |> IsarThy.theorem_i "" [inst_attribute add_thms] - (mk_prop (Theory.sign_of thy) sig_prop, []) int; + |> IsarThy.theorem_i (("", [inst_attribute add_thms], + (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int; val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms; val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms; @@ -430,13 +432,15 @@ val axclassP = OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl - (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [] -- Scan.repeat P.spec_name + (((P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) []) --| P.marg_comment) + -- Scan.repeat (P.spec_name --| P.marg_comment) >> (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.$$$ "<" |-- P.xname) >> instance_subclass_proof || - P.xname -- (P.$$$ "::" |-- P.simple_arity) >> (instance_arity_proof o P.triple2)) + ((P.xname -- (P.$$$ "<" |-- P.xname) -- P.marg_comment >> instance_subclass_proof || + (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment + >> instance_arity_proof) >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [axclassP, instanceP];