# HG changeset patch
# User wenzelm
# Date 935156605 -7200
# Node ID c065073cdb345a78fe2df591a6287698a3ac55f4
# Parent cd0533d52e55cfbb89ffa9840ea4ef1041c25410
eliminated HOL-AxClasses target;
diff -r cd0533d52e55 -r c065073cdb34 src/HOL/AxClasses/README.html
--- a/src/HOL/AxClasses/README.html Fri Aug 20 15:42:46 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-HOL/AxClasses/README
-
-Axiomatic type classes
-
-This directory contains the following axiomatic type class examples:
-
-
-
-
-- Tutorial
- Some simple axclass demos that go along with the
-axclass Isabelle document (isatool doc axclass).
-
-
-
-
- Group
-
- Some bits of group theory.
-
-
-
-
- Lattice
-
- Basic theory of lattices and orders.
-
-
-
-
diff -r cd0533d52e55 -r c065073cdb34 src/HOL/AxClasses/ROOT.ML
--- a/src/HOL/AxClasses/ROOT.ML Fri Aug 20 15:42:46 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Title: HOL/AxClasses/ROOT.ML
- ID: $Id$
- Author: Markus Wenzel
-
-Axiomatic type class examples.
-*)
-
-(*dummy file required for proper HTML generation*)
diff -r cd0533d52e55 -r c065073cdb34 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile Fri Aug 20 15:42:46 1999 +0200
+++ b/src/HOL/IsaMakefile Fri Aug 20 15:43:25 1999 +0200
@@ -9,8 +9,8 @@
default: HOL
images: HOL HOL-Real TLA
test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
- HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
- HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
+ HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
+ HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
TLA-Buffer TLA-Memory
@@ -254,17 +254,9 @@
@$(ISATOOL) usedir $(OUT)/HOL IOA
-## HOL-AxClasses
-
-HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
-
-$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/ROOT.ML
- @$(ISATOOL) usedir $(OUT)/HOL AxClasses
-
-
## HOL-AxClasses-Group
-HOL-AxClasses-Group: HOL-AxClasses $(LOG)/HOL-AxClasses-Group.gz
+HOL-AxClasses-Group: HOL $(LOG)/HOL-AxClasses-Group.gz
$(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
@@ -276,7 +268,7 @@
## HOL-AxClasses-Lattice
-HOL-AxClasses-Lattice: HOL-AxClasses $(LOG)/HOL-AxClasses-Lattice.gz
+HOL-AxClasses-Lattice: HOL $(LOG)/HOL-AxClasses-Lattice.gz
$(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
@@ -292,7 +284,7 @@
## HOL-AxClasses-Tutorial
-HOL-AxClasses-Tutorial: HOL-AxClasses $(LOG)/HOL-AxClasses-Tutorial.gz
+HOL-AxClasses-Tutorial: HOL $(LOG)/HOL-AxClasses-Tutorial.gz
$(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
AxClasses/Tutorial/BoolGroupInsts.thy AxClasses/Tutorial/Group.ML \
@@ -398,9 +390,10 @@
@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
$(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
$(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
- $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
- $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
- $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
+ $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
+ $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz \
+ $(LOG)/HOL-AxClasses-Group.gz \
+ $(LOG)/HOL-AxClasses-Lattice.gz \
$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
$(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
$(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \