diff -r c5c4884634b7 -r c7af682b9ee5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Aug 19 12:35:45 2004 +0200
+++ b/src/HOL/IsaMakefile	Fri Aug 20 12:20:09 2004 +0200
@@ -80,7 +80,8 @@
   $(SRC)/Provers/quasi.ML \
   $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
   $(SRC)/Provers/trancl.ML \
-  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
+  $(SRC)/TFL/isand.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 \
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
@@ -96,7 +97,8 @@
   Nat.thy NatArith.ML NatArith.thy \
   Power.thy PreList.thy Product_Type.ML Product_Type.thy \
   Refute.thy ROOT.ML \
-  Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
+  Recdef.thy Reconstruction.thy Record.thy\
+  Relation.ML Relation.thy Relation_Power.ML \
   Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
   Set.ML Set.thy SetInterval.ML SetInterval.thy \
   Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
@@ -107,7 +109,7 @@
   Tools/primrec_package.ML \
   Tools/prop_logic.ML \
   Tools/recdef_package.ML Tools/recfun_codegen.ML \
-  Tools/record_package.ML \
+  Tools/record_package.ML Tools/reconstruction.ML\
   Tools/refute.ML Tools/refute_isar.ML \
   Tools/rewrite_hol_proof.ML \
   Tools/sat_solver.ML \