changeset 5227 | e5a6ace920a0 |
parent 5148 | 74919e8f221c |
child 5278 | a903b66822e2 |
--- a/src/HOL/ex/MT.ML Fri Jul 31 10:54:39 1998 +0200 +++ b/src/HOL/ex/MT.ML Fri Jul 31 11:03:21 1998 +0200 @@ -15,8 +15,6 @@ NEEDS TO USE INDUCTIVE DEFS PACKAGE *) -open MT; - (* ############################################################ *) (* Inference systems *) (* ############################################################ *)