
diff -r db6ba2232945 -r 68324a8566c1 Tests/abacus.thy
--- 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
 




