Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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"
isabelle