formal comments (still dummy);
authorwenzelm
Tue May 25 20:24:10 1999 +0200 (1999-05-25)
changeset 6729b6e167580a32
parent 6728 b51b25db7bc6
child 6730 fa1f63249077
formal comments (still dummy);
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue May 25 20:23:30 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue May 25 20:24:10 1999 +0200
     1.3 @@ -670,7 +670,7 @@
     1.4  
     1.5  val datatype_decl =
     1.6    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
     1.7 -    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
     1.8 +    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment));
     1.9  
    1.10  fun mk_datatype args =
    1.11    let
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue May 25 20:23:30 1999 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue May 25 20:24:10 1999 +0200
     2.3 @@ -710,10 +710,11 @@
     2.4    #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
     2.5  
     2.6  fun ind_decl coind =
     2.7 -  Scan.repeat1 P.term --
     2.8 -  (P.$$$ "intrs" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term))) --
     2.9 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
    2.10 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) []
    2.11 +  (Scan.repeat1 P.term --| P.marg_comment) --
    2.12 +  (P.$$$ "intrs" |--
    2.13 +    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment))) --
    2.14 +  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
    2.15 +  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
    2.16    >> (Toplevel.theory o mk_ind coind);
    2.17  
    2.18  val inductiveP =
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Tue May 25 20:23:30 1999 +0200
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue May 25 20:24:10 1999 +0200
     3.3 @@ -265,7 +265,7 @@
     3.4  
     3.5  val primrec_decl =
     3.6    Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
     3.7 -    Scan.repeat1 (P.opt_thm_name ":" -- P.term);
     3.8 +    Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment);
     3.9  
    3.10  val primrecP =
    3.11    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
     4.1 --- a/src/HOL/Tools/recdef_package.ML	Tue May 25 20:23:30 1999 +0200
     4.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue May 25 20:24:10 1999 +0200
     4.3 @@ -139,7 +139,7 @@
     4.4  local structure P = OuterParse and K = OuterSyntax.Keyword in
     4.5  
     4.6  val recdef_decl =
     4.7 -  P.name -- P.term -- Scan.repeat1 P.term --
     4.8 +  P.name -- P.term -- Scan.repeat1 (P.term --| P.marg_comment) --
     4.9    Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
    4.10    Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
    4.11    >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
     5.1 --- a/src/HOL/Tools/record_package.ML	Tue May 25 20:23:30 1999 +0200
     5.2 +++ b/src/HOL/Tools/record_package.ML	Tue May 25 20:24:10 1999 +0200
     5.3 @@ -882,7 +882,7 @@
     5.4  
     5.5  val record_decl =
     5.6    P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+")
     5.7 -    -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ)));
     5.8 +    -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ) --| P.marg_comment));
     5.9  
    5.10  val recordP =
    5.11    OuterSyntax.command "record" "define extensible record" K.thy_decl
     6.1 --- a/src/HOL/Tools/typedef_package.ML	Tue May 25 20:23:30 1999 +0200
     6.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue May 25 20:24:10 1999 +0200
     6.3 @@ -15,9 +15,9 @@
     6.4      term -> string list -> thm list -> tactic option -> theory -> theory
     6.5    val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
     6.6      term -> string list -> thm list -> tactic option -> theory -> theory
     6.7 -  val typedef_proof: string -> bstring * string list * mixfix -> string
     6.8 +  val typedef_proof: (string * (bstring * string list * mixfix) * string) * Comment.text
     6.9      -> bool -> theory -> ProofHistory.T
    6.10 -  val typedef_proof_i: string -> bstring * string list * mixfix -> term
    6.11 +  val typedef_proof_i: (string * (bstring * string list * mixfix) * term) * Comment.text
    6.12      -> bool -> theory -> ProofHistory.T
    6.13  end;
    6.14  
    6.15 @@ -189,13 +189,13 @@
    6.16  fun typedef_attribute cset do_typedef (thy, thm) =
    6.17    (check_nonempty cset thm; (thy |> do_typedef, thm));
    6.18  
    6.19 -fun gen_typedef_proof prep_term name typ set int thy =
    6.20 +fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
    6.21    let
    6.22      val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
    6.23      val goal = Thm.term_of (goal_nonempty cset);
    6.24    in
    6.25      thy
    6.26 -    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) int
    6.27 +    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
    6.28    end;
    6.29  
    6.30  val typedef_proof = gen_typedef_proof read_term;
    6.31 @@ -209,16 +209,16 @@
    6.32  
    6.33  val typedeclP =
    6.34    OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl
    6.35 -    (P.type_args -- P.name -- P.opt_mixfix >> (fn ((vs, t), mx) =>
    6.36 +    (P.type_args -- P.name -- P.opt_mixfix --| P.marg_comment >> (fn ((vs, t), mx) =>
    6.37        Toplevel.theory (add_typedecls [(t, vs, mx)])));
    6.38  
    6.39  
    6.40  val typedef_proof_decl =
    6.41    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
    6.42 -    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term);
    6.43 +    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- P.marg_comment;
    6.44  
    6.45 -fun mk_typedef_proof (((opt_name, (vs, t)), mx), A) =
    6.46 -  typedef_proof (if_none opt_name (Syntax.type_name t mx)) (t, vs, mx) A;
    6.47 +fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), comment) =
    6.48 +  typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A), comment);
    6.49  
    6.50  val typedefP =
    6.51    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
     7.1 --- a/src/Pure/axclass.ML	Tue May 25 20:23:30 1999 +0200
     7.2 +++ b/src/Pure/axclass.ML	Tue May 25 20:24:10 1999 +0200
     7.3 @@ -30,10 +30,12 @@
     7.4      -> tactic option -> thm
     7.5    val goal_subclass: theory -> xclass * xclass -> thm list
     7.6    val goal_arity: theory -> xstring * xsort list * xclass -> thm list
     7.7 -  val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
     7.8 -  val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
     7.9 -  val instance_arity_proof: xstring * xsort list * xclass -> bool -> theory -> ProofHistory.T
    7.10 -  val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
    7.11 +  val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
    7.12 +  val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
    7.13 +  val instance_arity_proof: (xstring * xsort list * xclass) * Comment.text
    7.14 +    -> bool -> theory -> ProofHistory.T
    7.15 +  val instance_arity_proof_i: (string * sort list * class) * Comment.text
    7.16 +    -> bool -> theory -> ProofHistory.T
    7.17    val setup: (theory -> theory) list
    7.18  end;
    7.19  
    7.20 @@ -403,10 +405,10 @@
    7.21  
    7.22  fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
    7.23  
    7.24 -fun inst_proof mk_prop add_thms sig_prop int thy =
    7.25 +fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
    7.26    thy
    7.27 -  |> IsarThy.theorem_i "" [inst_attribute add_thms]
    7.28 -    (mk_prop (Theory.sign_of thy) sig_prop, []) int;
    7.29 +  |> IsarThy.theorem_i (("", [inst_attribute add_thms],
    7.30 +    (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int;
    7.31  
    7.32  val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
    7.33  val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;
    7.34 @@ -430,13 +432,15 @@
    7.35  
    7.36  val axclassP =
    7.37    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    7.38 -    (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [] -- Scan.repeat P.spec_name
    7.39 +    (((P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
    7.40 +      -- Scan.repeat (P.spec_name --| P.marg_comment)
    7.41        >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
    7.42  
    7.43  val instanceP =
    7.44    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    7.45 -    ((P.xname -- (P.$$$ "<" |-- P.xname) >> instance_subclass_proof ||
    7.46 -      P.xname -- (P.$$$ "::" |-- P.simple_arity) >> (instance_arity_proof o P.triple2))
    7.47 +    ((P.xname -- (P.$$$ "<" |-- P.xname) -- P.marg_comment >> instance_subclass_proof ||
    7.48 +      (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment
    7.49 +        >> instance_arity_proof)
    7.50        >> (Toplevel.print oo Toplevel.theory_to_proof));
    7.51  
    7.52  val _ = OuterSyntax.add_parsers [axclassP, instanceP];