constant dvd now in class target
authorhaftmann
Tue Jul 10 09:23:12 2007 +0200 (2007-07-10)
changeset 236869d5671f61b31
parent 23685 1b0f4071946c
child 23687 06884f7ffb18
constant dvd now in class target
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/HOL/divides.imp
     1.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Jul 10 09:23:11 2007 +0200
     1.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Jul 10 09:23:12 2007 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4  import_theory divides;
     1.5  
     1.6  const_maps
     1.7 -    divides > "Divides.dvd" :: "[nat,nat]=>bool";
     1.8 +  divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
     1.9  
    1.10  end_import;
    1.11  
     2.1 --- a/src/HOL/Import/HOL/divides.imp	Tue Jul 10 09:23:11 2007 +0200
     2.2 +++ b/src/HOL/Import/HOL/divides.imp	Tue Jul 10 09:23:12 2007 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  import_segment "hol4"
     2.5  
     2.6  const_maps
     2.7 -  "divides" > "Divides.dvd" :: "nat => nat => bool"
     2.8 +  "divides" > Divides.times_class.dvd :: "nat => nat => bool"
     2.9  
    2.10  thm_maps
    2.11    "divides_def" > "HOL4Compat.divides_def"