tracing disabled
authorwebertj
Sat Jun 02 00:09:02 2007 +0200 (2007-06-02)
changeset 23196fabf2e8a7ba4
parent 23195 f065f7c846fe
child 23197 f96d909eda37
tracing disabled
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/src/HOL/ex/Arith_Examples.thy	Fri Jun 01 23:52:06 2007 +0200
     1.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 00:09:02 2007 +0200
     1.3 @@ -26,7 +26,9 @@
     1.4    which {\tt fast_arith_tac} currently does not do.)
     1.5  *}
     1.6  
     1.7 +(*
     1.8  ML {* set trace_arith; *}
     1.9 +*)
    1.10  
    1.11  section {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    1.12             @{term HOL.minus}, @{term nat}, @{term Divides.mod},
    1.13 @@ -100,8 +102,6 @@
    1.14  lemma "(i::nat) div 0 = 0"
    1.15  oops
    1.16  
    1.17 -ML {* (#splits (ArithTheoryData.get (the_context ()))); *}
    1.18 -
    1.19  lemma "(i::nat) mod (number_of (1::int)) = 0"
    1.20  oops
    1.21  
    1.22 @@ -113,7 +113,7 @@
    1.23  lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
    1.24    by (tactic {* simple_arith_tac 1 *})
    1.25  
    1.26 -section {* Other Examples *}
    1.27 +section {* Various Other Examples *}
    1.28  
    1.29  lemma "[| (x::nat) < y; y < z |] ==> x < z"
    1.30    by (tactic {* fast_arith_tac 1 *})
    1.31 @@ -136,7 +136,7 @@
    1.32  lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
    1.33    by (tactic {* fast_arith_tac 1 *})
    1.34  
    1.35 -lemma "(x::nat) < y \<longrightarrow> P (x - y) \<longrightarrow> P 0"
    1.36 +lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
    1.37    by (tactic {* simple_arith_tac 1 *})
    1.38  
    1.39  lemma "(x - y) - (x::nat) = (x - x) - y"
    1.40 @@ -158,6 +158,8 @@
    1.41    a + b <= nat (max (abs i) (abs j))"
    1.42    by (tactic {* fast_arith_tac 1 *})
    1.43  
    1.44 +(*
    1.45  ML {* reset trace_arith; *}
    1.46 +*)
    1.47  
    1.48  end