# HG changeset patch
# User wenzelm
# Date 971904784 -7200
# Node ID bb66874b4750d30ebecacc2c0ac2c1dfc9088a54
# Parent  ed35c2b0e65cb73acc294e2932b02c2640b8d3ba
added HOL/Library, rearranged several files;

diff -r ed35c2b0e65c -r bb66874b4750 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 18 23:32:19 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 18 23:33:04 2000 +0200
@@ -9,8 +9,9 @@
 default: HOL
 images: HOL HOL-Real TLA
 
-#Note: keep targets sorted!
+#Note: keep targets sorted (except for HOL-Library)
 test: \
+  HOL-Library \
   HOL-Algebra \
   HOL-Auth \
   HOL-AxClasses \
@@ -57,43 +58,46 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		 \
-  $(SRC)/Provers/Arith/cancel_sums.ML		\
-  $(SRC)/Provers/Arith/assoc_fold.ML		\
-  $(SRC)/Provers/Arith/combine_numerals.ML	\
-  $(SRC)/Provers/Arith/cancel_numerals.ML	\
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+  $(SRC)/Provers/Arith/assoc_fold.ML \
+  $(SRC)/Provers/Arith/cancel_numerals.ML \
+  $(SRC)/Provers/Arith/cancel_sums.ML \
+  $(SRC)/Provers/Arith/combine_numerals.ML \
   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
-  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML \
-  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/rulify.ML \
-  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML \
-  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
-  $(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
-  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
-  NatArith.ML NatArith.thy Calculation.thy Datatype.thy Divides.ML \
-  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
-  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
-  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
-  Integ/IntArith.thy Integ/IntPower.ML Integ/IntPower.thy \
-  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
-  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
-  Integ/NatSimprocs.thy Integ/NatSimprocs.ML Integ/int_arith1.ML \
-  Integ/int_arith2.ML Integ/nat_simprocs.ML Lfp.ML Lfp.thy List.ML \
-  List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
-  NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
-  Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
-  Relation_Power.ML Relation_Power.thy Relation.ML Relation.thy Set.ML Set.thy \
-  SetInterval.ML SetInterval.thy String.thy SVC_Oracle.ML \
-  SVC_Oracle.thy Sum_Type.ML Sum_Type.thy Tools/datatype_aux.ML \
-  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
-  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
-  Tools/induct_method.ML Tools/inductive_package.ML Tools/meson.ML \
-  Tools/numeral_syntax.ML Tools/primrec_package.ML \
-  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
-  Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy Datatype_Universe.ML Datatype_Universe.thy \
-  Inverse_Image.ML Inverse_Image.thy Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML Wellfounded_Relations.thy While.ML \
-  While.thy arith_data.ML blastdata.ML cladata.ML equalities.ML \
-  equalities.thy hologic.ML meson_lemmas.ML mono.ML mono.thy simpdata.ML \
-  subset.ML subset.thy thy_syntax.ML
+  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
+  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/make_elim.ML \
+  $(SRC)/Provers/rulify.ML $(SRC)/Provers/simplifier.ML \
+  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
+  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
+  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sml \
+  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml Calculation.thy \
+  Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
+  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML \
+  HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
+  Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
+  Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \
+  Integ/IntDiv.ML Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \
+  Integ/NatBin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
+  Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
+  Integ/nat_simprocs.ML Inverse_Image.ML Inverse_Image.thy Lfp.ML \
+  Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
+  Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
+  Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy \
+  Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+  Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
+  SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
+  SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
+  Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
+  Tools/datatype_package.ML Tools/datatype_prop.ML \
+  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
+  Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
+  Tools/primrec_package.ML Tools/recdef_package.ML \
+  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
+  Transitive_Closure.ML Transitive_Closure.thy Wellfounded_Recursion.ML \
+  Wellfounded_Recursion.thy Wellfounded_Relations.ML \
+  Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
+  equalities.ML equalities.thy hologic.ML meson_lemmas.ML mono.ML \
+  mono.thy simpdata.ML subset.ML subset.thy thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
@@ -153,6 +157,17 @@
 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
 
 
+## HOL-Library
+
+HOL-Library: HOL $(LOG)/HOL-Library.gz
+
+$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.ML \
+  Library/Accessible_Part.thy Library/Library.thy Library/Multiset.thy \
+  Library/Quotient.thy Library/README.html Library/ROOT.ML \
+  Library/While_Combinator.thy Library/While_Combinator_Example.thy
+	@$(ISATOOL) usedir $(OUT)/HOL Library
+
+
 ## HOL-Subst
 
 HOL-Subst: HOL $(LOG)/HOL-Subst.gz
@@ -168,12 +183,10 @@
 
 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
 
-$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Acc.ML Induct/Acc.thy \
+$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
-  Induct/Multiset0.ML Induct/Multiset0.thy \
-  Induct/Multiset.ML Induct/Multiset.thy Induct/MultisetOrder.thy \
   Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
   Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
   Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
@@ -292,29 +305,25 @@
 
 HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
 
-$(LOG)/HOL-UNITY.gz: $(OUT)/HOL UNITY/ROOT.ML\
-  UNITY/AllocBase.ML UNITY/AllocBase.thy\
-  UNITY/Alloc.ML UNITY/Alloc.thy\
-  UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
-  UNITY/Client.ML UNITY/Client.thy  UNITY/Comp.ML UNITY/Comp.thy\
-  UNITY/Guar.ML UNITY/Guar.thy\
-  UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
-  UNITY/Detects.ML UNITY/Detects.thy\
-  UNITY/Reachability.ML UNITY/Reachability.thy\
-  UNITY/Union.ML UNITY/Union.thy UNITY/Handshake.ML UNITY/Handshake.thy\
-  UNITY/TimerArray.ML UNITY/TimerArray.thy\
-  UNITY/Extend.ML UNITY/Extend.thy UNITY/Project.ML UNITY/Project.thy\
-  UNITY/ELT.ML UNITY/ELT.thy\
-  UNITY/Follows.ML UNITY/Follows.thy\
-  UNITY/GenPrefix.thy UNITY/GenPrefix.ML \
-  UNITY/Lift_prog.ML UNITY/Lift_prog.thy UNITY/ListOrder.thy\
-  UNITY/Mutex.ML UNITY/Mutex.thy\
-  UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
-  UNITY/Rename.ML UNITY/Rename.thy\
-  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
-  UNITY/UNITY.ML UNITY/UNITY.thy\
-  UNITY/WFair.ML UNITY/WFair.thy UNITY/Lift.ML UNITY/Lift.thy\
-  UNITY/PPROD.ML UNITY/PPROD.thy UNITY/NSP_Bad.ML UNITY/NSP_Bad.thy
+$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/Alloc.ML \
+  UNITY/Alloc.thy UNITY/AllocBase.ML UNITY/AllocBase.thy \
+  UNITY/Channel.ML UNITY/Channel.thy UNITY/Client.ML UNITY/Client.thy \
+  UNITY/Common.ML UNITY/Common.thy UNITY/Comp.ML UNITY/Comp.thy \
+  UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/Detects.ML \
+  UNITY/Detects.thy UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \
+  UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
+  UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
+  UNITY/Guar.ML UNITY/Guar.thy UNITY/Handshake.ML UNITY/Handshake.thy \
+  UNITY/Lift.ML UNITY/Lift.thy UNITY/Lift_prog.ML UNITY/Lift_prog.thy \
+  UNITY/ListOrder.thy UNITY/Mutex.ML UNITY/Mutex.thy UNITY/NSP_Bad.ML \
+  UNITY/NSP_Bad.thy UNITY/Network.ML UNITY/Network.thy UNITY/PPROD.ML \
+  UNITY/PPROD.thy UNITY/Project.ML UNITY/Project.thy UNITY/ROOT.ML \
+  UNITY/Reach.ML UNITY/Reach.thy UNITY/Reachability.ML \
+  UNITY/Reachability.thy UNITY/Rename.ML UNITY/Rename.thy \
+  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/TimerArray.ML \
+  UNITY/TimerArray.thy UNITY/Token.ML UNITY/Token.thy UNITY/UNITY.ML \
+  UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML \
+  UNITY/WFair.thy
 	@$(ISATOOL) usedir $(OUT)/HOL UNITY
 
 
@@ -337,8 +346,8 @@
 
 HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
 
-$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Induct/Acc.thy Lambda/Commutation.thy \
-  Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
+$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
+  Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
   Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
   Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML Lambda/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL Lambda
@@ -468,8 +477,7 @@
   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
   Isar_examples/Group.thy Isar_examples/Hoare.thy Isar_examples/HoareEx.thy \
-  Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
-  Isar_examples/MutilatedCheckerboard.thy \
+  Isar_examples/KnasterTarski.thy Isar_examples/MutilatedCheckerboard.thy \
   Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \
   Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
   Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
@@ -539,4 +547,5 @@
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
-		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
+		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
+		$(LOG)/HOL-Library.gz