# HG changeset patch
# User wenzelm
# Date 957558317 -7200
# Node ID 7239b21e20682a76923f16dee0157fe567020852
# Parent  6ec0c8f9d68dc3832689519d464417caaf7b6476
removed Pure/section_utils.ML;

diff -r 6ec0c8f9d68d -r 7239b21e2068 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 05 22:24:47 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri May 05 22:25:17 2000 +0200
@@ -31,41 +31,40 @@
 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		\
-  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
-  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
-  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
-  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
-  $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \
-  $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig \
-  $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \
-  $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \
-  $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \
-  $(SRC)/TFL/utils.sml Arith.ML Arith.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/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.ML \
-  Lfp.ML Lfp.thy List.ML List.thy 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 Prod.ML \
-  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
-  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
-  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.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/numeral_syntax.ML Tools/primrec_package.ML \
-  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
-  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML  \
-  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
+$(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				\
+  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
+  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
+  $(SRC)/Provers/hypsubst.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/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml		\
+  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig		\
+  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml	\
+  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.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/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.ML Lfp.ML Lfp.thy List.ML List.thy 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 Prod.ML	\
+  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy		\
+  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy	\
+  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.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/numeral_syntax.ML Tools/primrec_package.ML			\
+  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML	\
+  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy	\
+  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML	\
+  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy	\
   simpdata.ML subset.ML subset.thy thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
diff -r 6ec0c8f9d68d -r 7239b21e2068 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri May 05 22:24:47 2000 +0200
+++ b/src/HOL/ROOT.ML	Fri May 05 22:25:17 2000 +0200
@@ -12,7 +12,6 @@
 print_depth 1;
 
 (*old-style theory syntax*)
-use "~~/src/Pure/section_utils.ML";
 use "thy_syntax.ML";
 
 use "hologic.ML";
diff -r 6ec0c8f9d68d -r 7239b21e2068 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri May 05 22:24:47 2000 +0200
+++ b/src/ZF/IsaMakefile	Fri May 05 22:25:17 2000 +0200
@@ -26,26 +26,24 @@
 FOL:
 	@cd $(SRC)/FOL; $(ISATOOL) make FOL
 
-$(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \
-  Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
-  CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \
-  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy \
-  Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \
-  Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy \
-  Let.ML Let.thy List.ML List.thy Main.thy Nat.ML Nat.thy \
-  Order.ML Order.thy OrderArith.ML \
-  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \
-  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
-  Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \
-  Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \
-  ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \
-  domrange.thy equalities.ML equalities.thy func.ML func.thy \
-  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
-  subset.thy thy_syntax.ML upair.ML upair.thy \
-  Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
-  Tools/primrec_package.ML Tools/induct_tacs.ML Tools/typechk.ML \
-  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
-  Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
+$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML Bool.thy	\
+  Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy		\
+  Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML	\
+  Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
+  Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML		\
+  Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	\
+  Integ/Int.thy Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy	\
+  Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML		\
+  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
+  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
+  Rel.ML Rel.thy Sum.ML Sum.thy Tools/cartprod.ML			\
+  Tools/datatype_package.ML Tools/induct_tacs.ML			\
+  Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML	\
+  Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
+  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy		\
+  equalities.ML equalities.thy func.ML func.thy ind_syntax.ML mono.ML	\
+  mono.thy pair.ML pair.thy simpdata.ML subset.ML subset.thy		\
+  thy_syntax.ML upair.ML upair.thy
 	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
 
 
diff -r 6ec0c8f9d68d -r 7239b21e2068 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Fri May 05 22:24:47 2000 +0200
+++ b/src/ZF/ROOT.ML	Fri May 05 22:25:17 2000 +0200
@@ -16,7 +16,6 @@
 print_depth 1;
 
 (*Add user sections for inductive/datatype definitions*)
-use     "~~/src/Pure/section_utils";
 use     "thy_syntax";
 
 use_thy "Let";