# HG changeset patch
# User wenzelm
# Date 1004133655 -7200
# Node ID b814360b0267d2286336eb32b2c23e5144e09230
# Parent  5818c5abb415ebcc398edab4ced8a16bbe8461fd
removed "more" class;

diff -r 5818c5abb415 -r b814360b0267 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