fixed Integ;
authorwenzelm
Thu Jul 02 16:44:39 1998 +0200 (1998-07-02)
changeset 51102497807020fa
parent 5109 b3d18eb3ac20
child 5111 8f4b72f0c15d
fixed Integ;
src/HOL/Integ/ROOT.ML
src/HOL/IsaMakefile
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/Integ/ROOT.ML	Wed Jul 01 19:11:20 1998 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,9 +0,0 @@
     1.4 -(*  Title:      HOL/Integ/ROOT
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1995  University of Cambridge
     1.8 -
     1.9 -The Integers in HOL (ported from ZF by Riccardo Mattolini)
    1.10 -*)
    1.11 -
    1.12 -time_use_thy "Bin";
     2.1 --- a/src/HOL/IsaMakefile	Wed Jul 01 19:11:20 1998 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Thu Jul 02 16:44:39 1998 +0200
     2.3 @@ -39,22 +39,19 @@
     2.4    $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
     2.5    $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
     2.6    $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
     2.7 -  Integ/Bin.ML Integ/Bin.thy  Integ/Equiv.ML Integ/Equiv.thy \
     2.8 -  Integ/Integ.ML Integ/Integ.thy Integ/ROOT.ML \
     2.9 -  Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \
    2.10 -  Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    2.11 -  Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
    2.12 +  Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
    2.13 +  Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
    2.14 +  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
    2.15 +  Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
    2.16    Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    2.17 -  Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
    2.18 +  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Record.thy RelPow.ML \
    2.19    RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    2.20 -  Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \
    2.21 -  Tools/inductive_package.ML \
    2.22 -  Trancl.ML Trancl.thy Univ.ML Univ.thy \
    2.23 -  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML \
    2.24 -  WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML cladata.ML \
    2.25 -  datatype.ML equalities.ML equalities.thy hologic.ML \
    2.26 -  mono.ML mono.thy \
    2.27 -  simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML
    2.28 +  Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
    2.29 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    2.30 +  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
    2.31 +  WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
    2.32 +  equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
    2.33 +  subset.thy thy_data.ML thy_syntax.ML
    2.34  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    2.35  
    2.36  
    2.37 @@ -342,7 +339,7 @@
    2.38  clean:
    2.39  	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    2.40  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    2.41 -	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    2.42 +	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    2.43  	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
    2.44  	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    2.45  	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
     3.1 --- a/src/HOL/ROOT.ML	Wed Jul 01 19:11:20 1998 +0200
     3.2 +++ b/src/HOL/ROOT.ML	Thu Jul 02 16:44:39 1998 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4  use_thy "Update";
     3.5  
     3.6  cd "Integ";
     3.7 -use "ROOT.ML";
     3.8 +use_thy "Bin";
     3.9  cd "..";
    3.10  
    3.11  (*TFL: recursive function definitions*)