--- a/src/HOL/ex/LList.ML Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/ex/LList.ML Thu Sep 12 10:40:05 1996 +0200
@@ -362,10 +362,10 @@
by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
qed "LCons_not_LNil";
-bind_thm ("LNil_not_LCons", (LCons_not_LNil RS not_sym));
+bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
-bind_thm ("LCons_neq_LNil", (LCons_not_LNil RS notE));
-val LNil_neq_LCons = sym RS LCons_neq_LNil;
+AddIffs [LCons_not_LNil, LNil_not_LCons];
+
(** llist constructors **)
@@ -392,14 +392,14 @@
(*For reasoning about abstract llist constructors*)
AddIs ([Rep_llist]@llist.intrs);
-AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
AddSDs [inj_onto_Abs_llist RS inj_ontoD,
- inj_Rep_llist RS injD, Leaf_inject];
+ inj_Rep_llist RS injD, Leaf_inject];
goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
by (Fast_tac 1);
qed "LCons_LCons_eq";
-bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
+
+AddIffs [LCons_LCons_eq];
val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
by (rtac (major RS llist.elim) 1);