src/HOL/Nat.thy
changeset 28952 15a4b2cf8c34
parent 28823 dcbef866c9e2
child 29608 564ea783ace8
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/Nat.thy	Wed Dec 03 09:53:58 2008 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Nat.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
     1.7  
     1.8  Type "nat" is a linear order, and a datatype; arithmetic operators + -
     1.9 @@ -13,7 +12,7 @@
    1.10  uses
    1.11    "~~/src/Tools/rat.ML"
    1.12    "~~/src/Provers/Arith/cancel_sums.ML"
    1.13 -  ("arith_data.ML")
    1.14 +  ("Tools/arith_data.ML")
    1.15    "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.16    ("Tools/lin_arith.ML")
    1.17  begin
    1.18 @@ -1323,7 +1322,7 @@
    1.19    shows "u = s"
    1.20    using 2 1 by (rule trans)
    1.21  
    1.22 -use "arith_data.ML"
    1.23 +use "Tools/arith_data.ML"
    1.24  declaration {* K ArithData.setup *}
    1.25  
    1.26  use "Tools/lin_arith.ML"