src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 44890 22f665a2e91c
parent 44241 7943b69f0188
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -49,11 +49,11 @@
     1.4  
     1.5  lemma subset_eq[code_pred_inline]:
     1.6    "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
     1.7 -by (rule eq_reflection) (fastsimp simp add: mem_def)
     1.8 +by (rule eq_reflection) (fastforce simp add: mem_def)
     1.9  
    1.10  lemma set_equality[code_pred_inline]:
    1.11    "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
    1.12 -by (fastsimp simp add: mem_def)
    1.13 +by (fastforce simp add: mem_def)
    1.14  
    1.15  section {* Setup for Numerals *}
    1.16  
    1.17 @@ -218,7 +218,7 @@
    1.18      unfolding mem_def[symmetric, of _ xc]
    1.19      apply auto
    1.20      unfolding mem_def
    1.21 -    apply fastsimp
    1.22 +    apply fastforce
    1.23      done
    1.24  qed
    1.25  
    1.26 @@ -240,7 +240,7 @@
    1.27      apply auto
    1.28      apply (case_tac xc)
    1.29      apply auto
    1.30 -    apply fastsimp
    1.31 +    apply fastforce
    1.32      done
    1.33  qed
    1.34