Mercurial Mercurial > hg > tm / 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.
tuned
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 14 Mar 2013 18:24:06 +0000
changeset 224 68324a8566c1
parent 223 db6ba2232945
child 225 0974c59e7029
tuned
Tests/abacus.thy file | annotate | diff | comparison | revisions 
--- a/Tests/abacus.thy	Thu Mar 14 18:02:26 2013 +0000
+++ b/Tests/abacus.thy	Thu Mar 14 18:24:06 2013 +0000
@@ -3,7 +3,7 @@
 *}
 
 theory abacus
-imports Main "~~/src/HOL/Algebra/IntRing" 
+imports Main
 begin
 
 text {*
@@ -159,7 +159,7 @@
 lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"
 apply (unfold Hoare_abc_def, clarify)
 apply (erule_tac x = "(a, aa, ab, b)" in allE)
-apply (erule_tac x = "r*ra" in allE) 
+apply (erule_tac x = "r * ra" in allE) 
 apply(simp add: stimes_ac)
 done
tm