# HG changeset patch
# User nipkow
# Date 795451777 -3600
# Node ID 136308504cd9c68bc8b7492d0ac8b3b0a4abed59
# Parent  932784dfa67138dff32af655f9088289213653f8
Added a few thms to nat_ss and list_ss

diff -r 932784dfa671 -r 136308504cd9 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Mar 17 15:35:09 1995 +0100
+++ b/src/HOL/List.ML	Fri Mar 17 15:49:37 1995 +0100
@@ -36,7 +36,8 @@
    map_Nil, map_Cons,
    flat_Nil, flat_Cons,
    list_all_Nil, list_all_Cons,
-   filter_Nil, filter_Cons];
+   filter_Nil, filter_Cons,
+   length_Nil, length_Cons];
 
 
 (** @ - append **)
@@ -117,6 +118,13 @@
 by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc])));
 qed"flat_append";
 
+(** length **)
+
+goal List.thy "length(xs@ys) = length(xs)+length(ys)";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+qed"length_append";
+
 (** nth **)
 
 val [nth_0,nth_Suc] = nat_recs nth_def; 
@@ -144,5 +152,5 @@
   [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
    mem_append, mem_filter,
    map_ident, map_append, map_compose,
-   flat_append, list_all_True, list_all_conj, nth_0, nth_Suc];
+   flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
 
diff -r 932784dfa671 -r 136308504cd9 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Mar 17 15:35:09 1995 +0100
+++ b/src/HOL/Nat.ML	Fri Mar 17 15:49:37 1995 +0100
@@ -433,4 +433,4 @@
 by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
 qed "Suc_le_mono";
 
-val nat_ss = nat_ss0 addsimps [le_refl];
+val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];