src/HOL/IsaMakefile
changeset 33318 ddd97d9dfbfb
parent 33298 dfda74619509
child 33333 78faaec3209f
child 33572 d78f347515e0
--- a/src/HOL/IsaMakefile	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Oct 29 11:41:36 2009 +0100
@@ -223,7 +223,6 @@
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
   Tools/split_rule.ML \
-  Tools/transfer.ML \
   Tools/typecopy.ML \
   Tools/typedef_codegen.ML \
   Tools/typedef.ML \
@@ -255,6 +254,7 @@
   Main.thy \
   Map.thy \
   Nat_Numeral.thy \
+  Nat_Transfer.thy \
   Presburger.thy \
   Predicate_Compile.thy \
   Quickcheck.thy \
@@ -276,6 +276,7 @@
   Tools/Groebner_Basis/misc.ML \
   Tools/Groebner_Basis/normalizer.ML \
   Tools/Groebner_Basis/normalizer_data.ML \
+  Tools/choice_specification.ML \
   Tools/int_arith.ML \
   Tools/list_code.ML \
   Tools/meson.ML \
@@ -299,7 +300,6 @@
   Tools/Qelim/presburger.ML \
   Tools/Qelim/qelim.ML \
   Tools/recdef.ML \
-  Tools/choice_specification.ML \
   Tools/res_atp.ML \
   Tools/res_axioms.ML \
   Tools/res_clause.ML \
@@ -307,6 +307,7 @@
   Tools/res_reconstruct.ML \
   Tools/string_code.ML \
   Tools/string_syntax.ML \
+  Tools/transfer.ML \
   Tools/TFL/casesplit.ML \
   Tools/TFL/dcterm.ML \
   Tools/TFL/post.ML \
@@ -334,7 +335,6 @@
   Log.thy \
   Lubs.thy \
   MacLaurin.thy \
-  Nat_Transfer.thy \
   NthRoot.thy \
   PReal.thy \
   Parity.thy \