src/HOL/IsaMakefile

   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \
   $(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 \
   Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
   Fun.thy Gfp.ML Gfp.thy Hilbert_Choice.thy HOL.ML \

   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
   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 \
   Tools/datatype_codegen.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/inductive_realizer.ML \
   Tools/meson.ML Tools/numeral_syntax.ML \
   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 \
   Tools/specification_package.ML \
   Tools/split_rule.ML Tools/typedef_package.ML \