author | wenzelm |
Wed, 20 Jul 1994 12:09:48 +0200 | |
changeset 480 | d74522d9437f |
parent 479 | db5a95f2952e |
child 481 | ac0568345f88 |
src/Pure/thm.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/thm.ML Mon Jul 18 12:24:35 1994 +0200 +++ b/src/Pure/thm.ML Wed Jul 20 12:09:48 1994 +0200 @@ -760,7 +760,7 @@ else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A} end; -(*Axiom-scheme reflecting signature contents: "(| ?'a::c : c_class |)". +(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)". Is weaker than some definition of c_class, e.g. "c_class == %x.T"; may be interpreted as an instance of A==>A.*) fun class_triv thy c =