Mercurial Mercurial > hg > regexp / 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.
Myhill_2.thy
changeset 160 ea2e5acbfe4a
parent 149 e122cb146ecc
child 162 e93760534354 
--- a/Myhill_2.thy	Wed May 04 07:05:59 2011 +0000
+++ b/Myhill_2.thy	Mon May 09 07:25:37 2011 +0000
@@ -661,7 +661,7 @@
         with eq_zab show ?thesis by simp
       qed
       with h5 h6 show ?thesis 
-        by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
   -- {* By instantiating the reasoning pattern just derived for both directions:*} 
@@ -770,7 +770,7 @@
         with z_decom show ?thesis by auto 
       qed
       with h5 h6 show ?thesis 
-        by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
   -- {* By instantiating the reasoning pattern just derived for both directions:*}
regexp