--- a/src/HOL/Induct/SList.ML Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/SList.ML Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
Definition of type 'a list by a least fixed point
*)
-open SList;
-
val list_con_defs = [NIL_def, CONS_def];
Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";