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
```