# HG changeset patch
# User wenzelm
# Date 1165775845 -3600
# Node ID 83b6cc133b287b703ee2f4e1fd2ecf5ba8dd564a
# Parent  5b76448793734020c114ba4161b475c73fc77c09
added Tools/string_syntax.ML;
tuned;

diff -r 5b7644879373 -r 83b6cc133b28 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Dec 10 17:37:55 2006 +0100
+++ b/src/HOL/IsaMakefile	Sun Dec 10 19:37:25 2006 +0100
@@ -70,71 +70,65 @@
   $(SRC)/Provers/Arith/cancel_sums.ML						\
   $(SRC)/Provers/Arith/combine_numerals.ML					\
   $(SRC)/Provers/Arith/extract_common_term.ML					\
-  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML		\
+  $(SRC)/Provers/Arith/fast_lin_arith.ML					\
+  $(SRC)/Provers/IsaPlanner/isand.ML						\
+  $(SRC)/Provers/IsaPlanner/rw_inst.ML						\
+  $(SRC)/Provers/IsaPlanner/rw_tools.ML						\
+  $(SRC)/Provers/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML			\
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
-  $(SRC)/Provers/IsaPlanner/zipper.ML \
-  $(SRC)/Provers/IsaPlanner/isand.ML \
-  $(SRC)/Provers/IsaPlanner/rw_tools.ML	\
-  $(SRC)/Provers/IsaPlanner/rw_inst.ML \
   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
   $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML			\
-  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML	\
-  $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
-  $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
-  $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
-  Tools/res_atpset.ML \
-  Code_Generator.thy Datatype.thy Divides.thy					\
-  Equiv_Relations.thy Extraction.thy Finite_Set.thy				\
-  FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
-  Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy				\
-  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
-  Integ/Presburger.thy Integ/cooper_dec.ML			\
-  Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
-  Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
-  Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
-  Lattices.thy List.thy Main.thy Map.thy Nat.thy Nat.ML OrderedGroup.ML		\
-  OrderedGroup.thy Orderings.thy Power.thy PreList.thy Product_Type.thy		\
-  ROOT.ML Recdef.thy Record.thy Refute.thy			\
-  Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy 			\
-  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
-  Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML 					\
-  Tools/cnf_funcs.ML					\
-  Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
-  Tools/datatype_codegen.ML Tools/datatype_hooks.ML Tools/datatype_package.ML	\
+  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML				\
+  $(SRC)/Provers/trancl.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML		\
+  $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML			\
+  $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML			\
+  $(SRC)/TFL/utils.ML ATP_Linkup.thy Accessible_Part.thy			\
+  Code_Generator.thy Datatype.thy Divides.thy Equiv_Relations.thy		\
+  Extraction.thy Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.ML	\
+  HOL.thy Hilbert_Choice.thy Inductive.thy Integ/IntArith.thy			\
+  Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy				\
+  Integ/NatSimprocs.thy Integ/Numeral.thy Integ/Presburger.thy			\
+  Integ/cooper_dec.ML Integ/cooper_proof.ML Integ/int_arith1.ML			\
+  Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Integ/presburger.ML	\
+  Integ/qelim.ML Integ/reflected_cooper.ML Integ/reflected_presburger.ML	\
+  LOrder.thy Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy		\
+  OrderedGroup.ML OrderedGroup.thy Orderings.thy Power.thy PreList.thy		\
+  Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy	\
+  Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy		\
+  Sum_Type.thy Tools/ATP/AtpCommunication.ML Tools/ATP/reduce_axiomsN.ML	\
+  Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML		\
+  Tools/datatype_aux.ML Tools/datatype_codegen.ML				\
+  Tools/datatype_hooks.ML Tools/datatype_package.ML				\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
-  Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
-  Tools/inductive_package.ML Tools/old_inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
-  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
-  Tools/polyhash.ML \
+  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML		\
+  Tools/function_package/context_tree.ML					\
+  Tools/function_package/fundef_common.ML					\
+  Tools/function_package/fundef_datatype.ML					\
+  Tools/function_package/fundef_lib.ML						\
+  Tools/function_package/fundef_package.ML					\
+  Tools/function_package/fundef_prep.ML						\
+  Tools/function_package/fundef_proof.ML					\
+  Tools/function_package/inductive_wrap.ML					\
+  Tools/function_package/lexicographic_order.ML					\
+  Tools/function_package/mutual.ML						\
+  Tools/function_package/pattern_split.ML					\
+  Tools/function_package/sum_tools.ML						\
+  Tools/function_package/termination.ML Tools/inductive_codegen.ML		\
+  Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
+  Tools/numeral_syntax.ML Tools/old_inductive_package.ML			\
+  Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
   Tools/recdef_package.ML Tools/recfun_codegen.ML				\
-  Tools/record_package.ML Tools/refute.ML		\
-  Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
-  Tools/res_clause.ML Tools/rewrite_hol_proof.ML	\
-  Tools/sat_funcs.ML					\
+  Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML			\
+  Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML		\
+  Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML			\
+  Tools/res_hol_clause.ML Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML		\
   Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
-  Tools/typecopy_package.ML	\
-  Tools/typedef_package.ML Tools/typedef_codegen.ML	\
-  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
-  Wellfounded_Relations.thy arith_data.ML			\
-  document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
-  Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
-  Tools/res_hol_clause.ML	\
-  Tools/function_package/sum_tools.ML 	\
-  Tools/function_package/fundef_common.ML 	\
-  Tools/function_package/fundef_lib.ML 	\
-  Tools/function_package/inductive_wrap.ML 	\
-  Tools/function_package/context_tree.ML 	\
-  Tools/function_package/fundef_prep.ML 	\
-  Tools/function_package/fundef_proof.ML 	\
-  Tools/function_package/termination.ML 	\
-  Tools/function_package/pattern_split.ML 	\
-  Tools/function_package/mutual.ML 	\
-  Tools/function_package/fundef_package.ML 	\
-  Tools/function_package/auto_term.ML 	\
-  Tools/function_package/lexicographic_order.ML 	\
-  Tools/function_package/fundef_datatype.ML 	\
-  FunDef.thy Accessible_Part.thy 
+  Tools/string_syntax.ML Tools/typecopy_package.ML				\
+  Tools/typedef_codegen.ML Tools/typedef_package.ML				\
+  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy			\
+  Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML		\
+  simpdata.ML
 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL