1.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jun 18 14:14:42 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jun 18 20:22:06 2010 +0200
     1.3 @@ -555,7 +555,6 @@
     1.4  apply auto
     1.5  apply (drule fold_steps_correct)
     1.6  apply (simp add: correctArray_def array_ran_def)
     1.7 -apply (cases "n = 0", auto)
     1.8  apply (rule implies_empty_inconsistent)
     1.9  apply (simp add:correctArray_def)
    1.10  apply (drule bspec)

     2.1 --- a/src/HOL/List.thy	Fri Jun 18 14:14:42 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Fri Jun 18 20:22:06 2010 +0200
     2.3 @@ -3190,6 +3190,9 @@
     2.4  lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
     2.5  by auto
     2.6  
     2.7 +lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \<noteq> 0)"
     2.8 +by (simp add: set_replicate_conv_if)
     2.9 +
    2.10  lemma Ball_set_replicate[simp]:
    2.11    "(ALL x : set(replicate n a). P x) = (P a | n=0)"
    2.12  by(simp add: set_replicate_conv_if)
    2.13 @@ -3198,9 +3201,6 @@
    2.14    "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
    2.15  by(simp add: set_replicate_conv_if)
    2.16  
    2.17 -lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
    2.18 -by (simp add: set_replicate_conv_if split: split_if_asm)
    2.19 -
    2.20  lemma replicate_append_same:
    2.21    "replicate i x @ [x] = x # replicate i x"
    2.22    by (induct i) simp_all

     3.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Jun 18 14:14:42 2010 +0200
     3.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Jun 18 20:22:06 2010 +0200
     3.3 @@ -2372,9 +2372,6 @@
     3.4  apply (simp add: check_type_simps)
     3.5  apply (simp only: list_def)
     3.6  apply (auto simp: err_def)
     3.7 -apply (subgoal_tac "set (replicate mxl Err) \<subseteq>  {Err}")
     3.8 -apply blast
     3.9 -apply (rule subset_replicate)
    3.10  done
    3.11  
    3.12  

     4.1 --- a/src/HOL/ex/Recdefs.thy	Fri Jun 18 14:14:42 2010 +0200
     4.2 +++ b/src/HOL/ex/Recdefs.thy	Fri Jun 18 20:22:06 2010 +0200
     4.3 @@ -120,11 +120,13 @@
     4.4  *}
     4.5  
     4.6  consts mapf :: "nat => nat list"
     4.7 -recdef (permissive) mapf  "measure (\<lambda>m. m)"
     4.8 +recdef mapf  "measure (\<lambda>m. m)"
     4.9    "mapf 0 = []"
    4.10    "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
    4.11    (hints cong: map_cong)
    4.12  
    4.13 +(* This used to be an example where recdef_tc etc is needed,
    4.14 +   but now termination is proved outright
    4.15  recdef_tc mapf_tc: mapf
    4.16    apply (rule allI)
    4.17    apply (case_tac "n = 0")
    4.18 @@ -138,5 +140,6 @@
    4.19    done
    4.20  
    4.21  lemmas mapf_induct = mapf.induct [OF mapf_tc]
    4.22 +*)
    4.23  
    4.24  end