# HG changeset patch
# User webertj
# Date 1180735742 -7200
# Node ID fabf2e8a7ba4689e6ff1d190268ccc44ee824936
# Parent  f065f7c846fe60be1f6f6c62a59449e4b3b9fbec
tracing disabled

diff -r f065f7c846fe -r fabf2e8a7ba4 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Fri Jun 01 23:52:06 2007 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 00:09:02 2007 +0200
@@ -26,7 +26,9 @@
   which {\tt fast_arith_tac} currently does not do.)
 *}
 
+(*
 ML {* set trace_arith; *}
+*)
 
 section {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
            @{term HOL.minus}, @{term nat}, @{term Divides.mod},
@@ -100,8 +102,6 @@
 lemma "(i::nat) div 0 = 0"
 oops
 
-ML {* (#splits (ArithTheoryData.get (the_context ()))); *}
-
 lemma "(i::nat) mod (number_of (1::int)) = 0"
 oops
 
@@ -113,7 +113,7 @@
 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
   by (tactic {* simple_arith_tac 1 *})
 
-section {* Other Examples *}
+section {* Various Other Examples *}
 
 lemma "[| (x::nat) < y; y < z |] ==> x < z"
   by (tactic {* fast_arith_tac 1 *})
@@ -136,7 +136,7 @@
 lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
   by (tactic {* fast_arith_tac 1 *})
 
-lemma "(x::nat) < y \<longrightarrow> P (x - y) \<longrightarrow> P 0"
+lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
   by (tactic {* simple_arith_tac 1 *})
 
 lemma "(x - y) - (x::nat) = (x - x) - y"
@@ -158,6 +158,8 @@
   a + b <= nat (max (abs i) (abs j))"
   by (tactic {* fast_arith_tac 1 *})
 
+(*
 ML {* reset trace_arith; *}
+*)
 
 end