# HG changeset patch
# User wenzelm
# Date 1337781432 -7200
# Node ID b8a94ed1646e8b2db896e592fb8ce3e5bc336421
# Parent  b74655182ed6c226400c957ac839f127fe70438d
eliminated obsolete fastsimp;

diff -r b74655182ed6 -r b8a94ed1646e src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed May 23 15:40:10 2012 +0200
+++ b/src/CCL/CCL.thy	Wed May 23 15:57:12 2012 +0200
@@ -349,7 +349,7 @@
 
 lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))"
   apply (rule poXH [THEN iff_trans])
-  apply fastsimp
+  apply fastforce
   done
 
 lemmas ccl_porews = po_bot po_pair po_lam
diff -r b74655182ed6 -r b8a94ed1646e src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Wed May 23 15:40:10 2012 +0200
+++ b/src/CCL/Hered.thy	Wed May 23 15:57:12 2012 +0200
@@ -118,13 +118,13 @@
   by (simp add: subsetXH UnitXH HTT_rews)
 
 lemma BoolF: "Bool <= HTT"
-  by (fastsimp simp: subsetXH BoolXH iff: HTT_rews)
+  by (fastforce simp: subsetXH BoolXH iff: HTT_rews)
 
 lemma PlusF: "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT"
-  by (fastsimp simp: subsetXH PlusXH iff: HTT_rews)
+  by (fastforce simp: subsetXH PlusXH iff: HTT_rews)
 
 lemma SigmaF: "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"
-  by (fastsimp simp: subsetXH SgXH HTT_rews)
+  by (fastforce simp: subsetXH SgXH HTT_rews)
 
 
 (*** Formation Rules for Recursive types - using coinduction these only need ***)
@@ -135,7 +135,7 @@
   apply (simp add: subsetXH)
   apply clarify
   apply (erule Nat_ind)
-   apply (fastsimp iff: HTT_rews)+
+   apply (fastforce iff: HTT_rews)+
   done
 
 lemma NatF: "Nat <= HTT"
diff -r b74655182ed6 -r b8a94ed1646e src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Wed May 23 15:40:10 2012 +0200
+++ b/src/CCL/Wfd.thy	Wed May 23 15:57:12 2012 +0200
@@ -209,18 +209,18 @@
   apply (unfold Wfd_def)
   apply clarify
   apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
-   apply (fastsimp iff: NatPRXH)
+   apply (fastforce iff: NatPRXH)
   apply (erule Nat_ind)
-   apply (fastsimp iff: NatPRXH)+
+   apply (fastforce iff: NatPRXH)+
   done
 
 lemma ListPR_wf: "Wfd(ListPR(A))"
   apply (unfold Wfd_def)
   apply clarify
   apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
-   apply (fastsimp iff: ListPRXH)
+   apply (fastforce iff: ListPRXH)
   apply (erule List_ind)
-   apply (fastsimp iff: ListPRXH)+
+   apply (fastforce iff: ListPRXH)+
   done
 
 
diff -r b74655182ed6 -r b8a94ed1646e src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Wed May 23 15:40:10 2012 +0200
+++ b/src/CCL/ex/Stream.thy	Wed May 23 15:57:12 2012 +0200
@@ -33,7 +33,7 @@
   apply safe
   apply (drule ListsXH [THEN iffD1])
   apply (tactic "EQgen_tac @{context} [] 1")
-   apply fastsimp
+   apply fastforce
   done
 
 (*** Mapping the identity function leaves a list unchanged ***)