--- a/src/HOL/ex/BinEx.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/BinEx.thy Sun Oct 01 18:29:23 2006 +0200
@@ -10,9 +10,6 @@
subsection {* Regression Testing for Cancellation Simprocs *}
-(*taken from HOL/Integ/int_arith1.ML *)
-
-
lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
apply simp oops
@@ -283,7 +280,7 @@
lemma "Suc 99999 = 100000"
by (simp add: Suc_nat_number_of)
- -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
+ -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
text {* \medskip Addition *}
@@ -390,8 +387,4 @@
lemma "x + y - x + z - x - y - z + x < (1::int)"
by simp
-
-text{*The proofs about arithmetic yielding normal forms have been deleted:
- they are irrelevant with the new treatment of numerals.*}
-
end