--- 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];