oops;

--- a/src/HOL/List.ML	Wed May 08 10:15:04 2002 +0200
+++ b/src/HOL/List.ML	Wed May 08 12:15:30 2002 +0200
@@ -191,7 +191,6 @@
 val rev_concat = thm "rev_concat";
 val rev_drop = thm "rev_drop";
 val rev_exhaust = thm "rev_exhaust";
-val rev_exhaust_aux = thm "rev_exhaust_aux";
 val rev_induct = thm "rev_induct";
 val rev_is_Nil_conv = thm "rev_is_Nil_conv";
 val rev_is_rev_conv = thm "rev_is_rev_conv";

--- a/src/HOL/List.thy	Wed May 08 10:15:04 2002 +0200
+++ b/src/HOL/List.thy	Wed May 08 12:15:30 2002 +0200
@@ -5,7 +5,8 @@
 *)
 
 header {* The datatype of finite lists *}
-theory List1 = PreList:
+
+theory List = PreList:
 
 datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)
 
@@ -210,7 +211,7 @@
 
 lemmas not_Cons_self2[simp] = not_Cons_self[THEN not_sym]
 
-lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)";
+lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)"
 by(induct_tac "xs", auto)
 
 (* Induction over the length of a list: *)
@@ -229,7 +230,7 @@
 declare lists.intros[intro!]
 
 lemma lists_IntI[rule_format]:
- "l: lists A ==> l: lists B --> l: lists (A Int B)";
+ "l: lists A ==> l: lists B --> l: lists (A Int B)"
 apply(erule lists.induct)
 apply blast+
 done
@@ -358,6 +359,12 @@
 ML_setup{*
 local
 
+val append_assoc = thm "append_assoc";
+val append_Nil = thm "append_Nil";
+val append_Cons = thm "append_Cons";
+val append1_eq_conv = thm "append1_eq_conv";
+val append_same_eq = thm "append_same_eq";
+
 val list_eq_pattern =
   Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
 
@@ -1344,4 +1351,4 @@
                 drop_Cons'[of "number_of v",standard]
                 nth_Cons'[of "number_of v",standard]
 
-end;
+end