eliminated HOL-AxClasses target;
authorwenzelm
Fri Aug 20 15:43:25 1999 +0200 (1999-08-20)
changeset 7307c065073cdb34
parent 7306 cd0533d52e55
child 7308 e01aab03a2a1
eliminated HOL-AxClasses target;
src/HOL/AxClasses/README.html
src/HOL/AxClasses/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/AxClasses/README.html	Fri Aug 20 15:42:46 1999 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,25 +0,0 @@
     1.4 -<HTML><HEAD><TITLE>HOL/AxClasses/README</TITLE></HEAD><BODY>
     1.5 -
     1.6 -<h2>Axiomatic type classes</h2>
     1.7 -
     1.8 -This directory contains the following axiomatic type class examples:
     1.9 -
    1.10 -
    1.11 -<DL>
    1.12 -
    1.13 -<DT> Tutorial <DD> Some simple axclass demos that go along with the
    1.14 -<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
    1.15 -
    1.16 -<P>
    1.17 -
    1.18 -<DT> Group
    1.19 -<DD> Some bits of group theory.
    1.20 -
    1.21 -<P>
    1.22 -
    1.23 -<DT> Lattice
    1.24 -<DD> Basic theory of lattices and orders.
    1.25 -
    1.26 -</DL>
    1.27 -
    1.28 -</BODY></HTML>
     2.1 --- a/src/HOL/AxClasses/ROOT.ML	Fri Aug 20 15:42:46 1999 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,8 +0,0 @@
     2.4 -(*  Title:      HOL/AxClasses/ROOT.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel
     2.7 -
     2.8 -Axiomatic type class examples.
     2.9 -*)
    2.10 -
    2.11 -(*dummy file required for proper HTML generation*)
     3.1 --- a/src/HOL/IsaMakefile	Fri Aug 20 15:42:46 1999 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Fri Aug 20 15:43:25 1999 +0200
     3.3 @@ -9,8 +9,8 @@
     3.4  default: HOL
     3.5  images: HOL HOL-Real TLA
     3.6  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
     3.7 -  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
     3.8 -  HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
     3.9 +  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
    3.10 +  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
    3.11    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
    3.12    TLA-Buffer TLA-Memory
    3.13  
    3.14 @@ -254,17 +254,9 @@
    3.15  	@$(ISATOOL) usedir $(OUT)/HOL IOA
    3.16  
    3.17  
    3.18 -## HOL-AxClasses
    3.19 -
    3.20 -HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
    3.21 -
    3.22 -$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/ROOT.ML
    3.23 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
    3.24 -
    3.25 -
    3.26  ## HOL-AxClasses-Group
    3.27  
    3.28 -HOL-AxClasses-Group: HOL-AxClasses $(LOG)/HOL-AxClasses-Group.gz
    3.29 +HOL-AxClasses-Group: HOL $(LOG)/HOL-AxClasses-Group.gz
    3.30  
    3.31  $(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
    3.32    AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
    3.33 @@ -276,7 +268,7 @@
    3.34  
    3.35  ## HOL-AxClasses-Lattice
    3.36  
    3.37 -HOL-AxClasses-Lattice: HOL-AxClasses $(LOG)/HOL-AxClasses-Lattice.gz
    3.38 +HOL-AxClasses-Lattice: HOL $(LOG)/HOL-AxClasses-Lattice.gz
    3.39  
    3.40  $(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
    3.41    AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
    3.42 @@ -292,7 +284,7 @@
    3.43  
    3.44  ## HOL-AxClasses-Tutorial
    3.45  
    3.46 -HOL-AxClasses-Tutorial: HOL-AxClasses $(LOG)/HOL-AxClasses-Tutorial.gz
    3.47 +HOL-AxClasses-Tutorial: HOL $(LOG)/HOL-AxClasses-Tutorial.gz
    3.48  
    3.49  $(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
    3.50    AxClasses/Tutorial/BoolGroupInsts.thy AxClasses/Tutorial/Group.ML \
    3.51 @@ -398,9 +390,10 @@
    3.52  	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    3.53  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    3.54  	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    3.55 -	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
    3.56 -	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    3.57 -	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
    3.58 +	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    3.59 +	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz \
    3.60 +	  $(LOG)/HOL-AxClasses-Group.gz		\
    3.61 +	  $(LOG)/HOL-AxClasses-Lattice.gz	\
    3.62  	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
    3.63  	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
    3.64  	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \