| changeset 5210 | 54aaa779b6b4 |
| parent 5198 | b1adae4f8b90 |
| child 5694 | 39af7b3dd1c4 |
--- a/src/HOL/Record.thy Tue Jul 28 17:03:12 1998 +0200 +++ b/src/HOL/Record.thy Tue Jul 28 17:05:34 1998 +0200 @@ -42,12 +42,8 @@ (* type class for record extensions *) -global (*compatibility with global_names flag!*) - axclass more < term -local - instance unit :: more instance "*" :: (term, more) more