src/HOL/List.thy
changeset 13122 c63612ffb186
parent 13114 f2b00262bdfc
child 13124 6e1decd8a7a9
     1.1 --- a/src/HOL/List.thy	Wed May 08 10:15:04 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Wed May 08 12:15:30 2002 +0200
     1.3 @@ -5,7 +5,8 @@
     1.4  *)
     1.5  
     1.6  header {* The datatype of finite lists *}
     1.7 -theory List1 = PreList:
     1.8 +
     1.9 +theory List = PreList:
    1.10  
    1.11  datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)
    1.12  
    1.13 @@ -210,7 +211,7 @@
    1.14  
    1.15  lemmas not_Cons_self2[simp] = not_Cons_self[THEN not_sym]
    1.16  
    1.17 -lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)";
    1.18 +lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)"
    1.19  by(induct_tac "xs", auto)
    1.20  
    1.21  (* Induction over the length of a list: *)
    1.22 @@ -229,7 +230,7 @@
    1.23  declare lists.intros[intro!]
    1.24  
    1.25  lemma lists_IntI[rule_format]:
    1.26 - "l: lists A ==> l: lists B --> l: lists (A Int B)";
    1.27 + "l: lists A ==> l: lists B --> l: lists (A Int B)"
    1.28  apply(erule lists.induct)
    1.29  apply blast+
    1.30  done
    1.31 @@ -358,6 +359,12 @@
    1.32  ML_setup{*
    1.33  local
    1.34  
    1.35 +val append_assoc = thm "append_assoc";
    1.36 +val append_Nil = thm "append_Nil";
    1.37 +val append_Cons = thm "append_Cons";
    1.38 +val append1_eq_conv = thm "append1_eq_conv";
    1.39 +val append_same_eq = thm "append_same_eq";
    1.40 +
    1.41  val list_eq_pattern =
    1.42    Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
    1.43  
    1.44 @@ -1344,4 +1351,4 @@
    1.45                  drop_Cons'[of "number_of v",standard]
    1.46                  nth_Cons'[of "number_of v",standard]
    1.47  
    1.48 -end;
    1.49 +end