oops;
authorwenzelm
Wed May 08 12:15:30 2002 +0200 (2002-05-08)
changeset 13122c63612ffb186
parent 13121 4888694b2829
child 13123 777db68dee1e
oops;
src/HOL/List.ML
src/HOL/List.thy
     1.1 --- a/src/HOL/List.ML	Wed May 08 10:15:04 2002 +0200
     1.2 +++ b/src/HOL/List.ML	Wed May 08 12:15:30 2002 +0200
     1.3 @@ -191,7 +191,6 @@
     1.4  val rev_concat = thm "rev_concat";
     1.5  val rev_drop = thm "rev_drop";
     1.6  val rev_exhaust = thm "rev_exhaust";
     1.7 -val rev_exhaust_aux = thm "rev_exhaust_aux";
     1.8  val rev_induct = thm "rev_induct";
     1.9  val rev_is_Nil_conv = thm "rev_is_Nil_conv";
    1.10  val rev_is_rev_conv = thm "rev_is_rev_conv";
     2.1 --- a/src/HOL/List.thy	Wed May 08 10:15:04 2002 +0200
     2.2 +++ b/src/HOL/List.thy	Wed May 08 12:15:30 2002 +0200
     2.3 @@ -5,7 +5,8 @@
     2.4  *)
     2.5  
     2.6  header {* The datatype of finite lists *}
     2.7 -theory List1 = PreList:
     2.8 +
     2.9 +theory List = PreList:
    2.10  
    2.11  datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)
    2.12  
    2.13 @@ -210,7 +211,7 @@
    2.14  
    2.15  lemmas not_Cons_self2[simp] = not_Cons_self[THEN not_sym]
    2.16  
    2.17 -lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)";
    2.18 +lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)"
    2.19  by(induct_tac "xs", auto)
    2.20  
    2.21  (* Induction over the length of a list: *)
    2.22 @@ -229,7 +230,7 @@
    2.23  declare lists.intros[intro!]
    2.24  
    2.25  lemma lists_IntI[rule_format]:
    2.26 - "l: lists A ==> l: lists B --> l: lists (A Int B)";
    2.27 + "l: lists A ==> l: lists B --> l: lists (A Int B)"
    2.28  apply(erule lists.induct)
    2.29  apply blast+
    2.30  done
    2.31 @@ -358,6 +359,12 @@
    2.32  ML_setup{*
    2.33  local
    2.34  
    2.35 +val append_assoc = thm "append_assoc";
    2.36 +val append_Nil = thm "append_Nil";
    2.37 +val append_Cons = thm "append_Cons";
    2.38 +val append1_eq_conv = thm "append1_eq_conv";
    2.39 +val append_same_eq = thm "append_same_eq";
    2.40 +
    2.41  val list_eq_pattern =
    2.42    Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
    2.43  
    2.44 @@ -1344,4 +1351,4 @@
    2.45                  drop_Cons'[of "number_of v",standard]
    2.46                  nth_Cons'[of "number_of v",standard]
    2.47  
    2.48 -end;
    2.49 +end