src/CCL/Hered.thy
 changeset 47966 b8a94ed1646e parent 42156 df219e736a5d child 58889 5b7a9633cfa8
```--- 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"```