removed "more" class;
authorwenzelm
Sat, 27 Oct 2001 00:00:55 +0200
changeset 11956 b814360b0267
parent 11955 5818c5abb415
child 11957 f1657e0291ca
removed "more" class;
src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sat Oct 27 00:00:38 2001 +0200
+++ b/src/HOL/Record.thy	Sat Oct 27 00:00:55 2001 +0200
@@ -126,12 +126,6 @@
 qed
 
 
-subsection {* Type class for record extensions *}
-
-axclass more < "term"
-instance unit :: more ..
-
-
 subsection {* Concrete record syntax *}
 
 nonterminals