Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped
authorberghofe
Wed, 07 May 2008 10:59:39 +0200
changeset 26824 32e612e77edb
parent 26823 f426b9c2a90d
child 26825 0373ed6f04b1
Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.
src/HOL/UNITY/Simple/Deadlock.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Simple/Deadlock.thy	Wed May 07 10:59:38 2008 +0200
+++ b/src/HOL/UNITY/Simple/Deadlock.thy	Wed May 07 10:59:39 2008 +0200
@@ -35,7 +35,7 @@
      "(\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i))  \<subseteq>  
       (\<Inter>i \<in> lessThan n. -A i) \<union> A n"
 apply (induct_tac "n", simp)
-apply (simp add: lessThan_Suc, blast)
+apply (simp add: lessThan_Suc, fast)
 done
isabelle