src/HOL/Nat.thy
changeset 35047 1b2bae06c796
parent 35028 108662d50512
child 35064 1bdef0c013d3
     1.1 --- a/src/HOL/Nat.thy	Mon Feb 08 17:12:24 2010 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Feb 08 17:12:27 2010 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Natural numbers *}
     1.5  
     1.6  theory Nat
     1.7 -imports Inductive Product_Type Ring_and_Field
     1.8 +imports Inductive Product_Type Fields
     1.9  uses
    1.10    "~~/src/Tools/rat.ML"
    1.11    "~~/src/Provers/Arith/cancel_sums.ML"
    1.12 @@ -176,6 +176,8 @@
    1.13  
    1.14  end
    1.15  
    1.16 +hide (open) fact add_0_right
    1.17 +
    1.18  instantiation nat :: comm_semiring_1_cancel
    1.19  begin
    1.20  
    1.21 @@ -730,7 +732,7 @@
    1.22    apply (induct n)
    1.23    apply (simp_all add: order_le_less)
    1.24    apply (blast elim!: less_SucE
    1.25 -               intro!: add_0_right [symmetric] add_Suc_right [symmetric])
    1.26 +               intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
    1.27    done
    1.28  
    1.29  text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}