src/HOL/Integ/IntDiv.thy
changeset 15131 c69542757a4d
parent 15101 d027515e2aa6
child 15140 322485b816ac
     1.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Aug 16 14:21:54 2004 +0200
     1.2 +++ b/src/HOL/Integ/IntDiv.thy	Mon Aug 16 14:22:27 2004 +0200
     1.3 @@ -31,8 +31,10 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -theory IntDiv = IntArith + Recdef
     1.8 -  files ("IntDiv_setup.ML"):
     1.9 +theory IntDiv
    1.10 +import IntArith Recdef
    1.11 +files ("IntDiv_setup.ML")
    1.12 +begin
    1.13  
    1.14  declare zless_nat_conj [simp]
    1.15