src/HOL/IsaMakefile

   HOL-Algebra \
   HOL-Auth \
   HOL-AxClasses \
   HOL-Bali \
   HOL-CTL \
+  HOL-Extraction \
   HOL-GroupTheory \
       HOL-Real-HahnBanach \
       HOL-Real-ex \
   HOL-Hoare \
   HOL-HoareParallel \

   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
   $(SRC)/Provers/splitter.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 \
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
-  Divides.thy Finite_Set.ML Finite_Set.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
+  Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
+  Fun.ML Fun.thy Gfp.ML Gfp.thy \
   Hilbert_Choice.thy Hilbert_Choice_lemmas.ML 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.thy Integ/IntPower.ML Integ/IntPower.thy \

   Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
   Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
   Tools/datatype_rep_proofs.ML \
   Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \
   Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
-  Tools/record_package.ML Tools/split_rule.ML Tools/typedef_package.ML \
+  Tools/record_package.ML Tools/rewrite_hol_proof.ML \
+  Tools/split_rule.ML Tools/typedef_package.ML \
   Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
   Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
   document/root.tex hologic.ML meson_lemmas.ML simpdata.ML thy_syntax.ML
 	@$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL

 $(LOG)/HOL-CTL.gz: $(OUT)/HOL \
   CTL/CTL.thy CTL/ROOT.ML CTL/document/root.tex CTL/document/root.bib
 	@$(ISATOOL) usedir $(OUT)/HOL CTL
 
 
+## HOL-Extraction
+
+HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
+
+$(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
+  Extraction/Higman.thy Extraction/ROOT.ML Extraction/QuotRem.thy \
+  Extraction/Warshall.thy Extraction/document/root.tex \
+  Extraction/document/root.bib
+	@$(ISATOOL) usedir $(OUT)/HOL Extraction
+
+
 ## HOL-IOA
 
 HOL-IOA: HOL $(LOG)/HOL-IOA.gz
 
 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.ML IOA/Asig.thy IOA/IOA.ML \