1.1 --- a/src/HOL/Bali/Example.thy	Mon May 18 09:48:06 2009 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Mon May 18 23:15:38 2009 +0200
     1.3 @@ -1075,7 +1075,7 @@
     1.4  lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
     1.5    {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
     1.6     , [Class Base])}"
     1.7 -by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
     1.8 +by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
     1.9  
    1.10  section "well-typedness"
    1.11  

     2.1 --- a/src/HOL/Library/Pocklington.thy	Mon May 18 09:48:06 2009 +0200
     2.2 +++ b/src/HOL/Library/Pocklington.thy	Mon May 18 23:15:38 2009 +0200
     2.3 @@ -382,8 +382,9 @@
     2.4  (* Euler totient function.                                                   *)
     2.5  
     2.6  definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
     2.7 +
     2.8  lemma phi_0[simp]: "\<phi> 0 = 0"
     2.9 -  unfolding phi_def by (auto simp add: card_eq_0_iff)
    2.10 +  unfolding phi_def by auto
    2.11  
    2.12  lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
    2.13  proof-

     3.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon May 18 09:48:06 2009 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon May 18 23:15:38 2009 +0200
     3.3 @@ -69,9 +69,9 @@
     3.4  lemma subcls1:
     3.5    "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
     3.6                  (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
     3.7 -apply (simp add: subcls1_def2 del:singleton_conj_conv2)
     3.8 +apply (simp add: subcls1_def2)
     3.9  apply (simp add: name_defs class_defs system_defs E_def class_def)
    3.10 -apply (auto simp: expand_fun_eq split: split_if_asm)
    3.11 +apply (auto simp: expand_fun_eq)
    3.12  done
    3.13  
    3.14  text {* The subclass relation is acyclic; hence its converse is well founded: *}

     4.1 --- a/src/HOL/Set.thy	Mon May 18 09:48:06 2009 +0200
     4.2 +++ b/src/HOL/Set.thy	Mon May 18 23:15:38 2009 +0200
     4.3 @@ -1036,12 +1036,17 @@
     4.4  
     4.5  text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
     4.6  
     4.7 -lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
     4.8 +lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
     4.9  by auto
    4.10  
    4.11 -lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
    4.12 +lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
    4.13  by auto
    4.14  
    4.15 +text {*
    4.16 +Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
    4.17 +to the front (and similarly for @{text "t=x"}):
    4.18 +*}
    4.19 +
    4.20  ML{*
    4.21    local
    4.22      val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    4.23 @@ -1054,7 +1059,6 @@
    4.24    end;
    4.25  
    4.26    Addsimprocs [defColl_regroup];
    4.27 -
    4.28  *}
    4.29  
    4.30  text {*

     5.1 --- a/src/Provers/quantifier1.ML	Mon May 18 09:48:06 2009 +0200
     5.2 +++ b/src/Provers/quantifier1.ML	Mon May 18 23:15:38 2009 +0200
     5.3 @@ -90,7 +90,7 @@
     5.4  
     5.5  fun extract_conj fst xs t = case dest_conj t of NONE => NONE
     5.6      | SOME(conj,P,Q) =>
     5.7 -        (if not fst andalso def xs P then SOME(xs,P,Q) else
     5.8 +        (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
     5.9           if def xs Q then SOME(xs,Q,P) else
    5.10           (case extract_conj false xs P of
    5.11              SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
    5.12 @@ -99,7 +99,7 @@
    5.13                       | NONE => NONE)));
    5.14  
    5.15  fun extract_imp fst xs t = case dest_imp t of NONE => NONE
    5.16 -    | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
    5.17 +    | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
    5.18                         else (case extract_conj false xs P of
    5.19                                 SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
    5.20                               | NONE => (case extract_imp false xs Q of