use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
authorblanchet
Tue May 31 16:38:36 2011 +0200 (2011-05-31)
changeset 43108eb1e31eb7449
parent 43107 5792d6bb4fb1
child 43109 8c9046951dcb
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
src/HOL/ATP.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/ATP.thy	Tue May 31 16:38:36 2011 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue May 31 16:38:36 2011 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  theory ATP
     1.6  imports Meson
     1.7 -uses "Tools/ATP/atp_util.ML"
     1.8 +uses "Tools/monomorph.ML"
     1.9 +     "Tools/ATP/atp_util.ML"
    1.10       "Tools/ATP/atp_problem.ML"
    1.11       "Tools/ATP/atp_proof.ML"
    1.12       "Tools/ATP/atp_systems.ML"
     2.1 --- a/src/HOL/IsaMakefile	Tue May 31 16:38:36 2011 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue May 31 16:38:36 2011 +0200
     2.3 @@ -310,6 +310,7 @@
     2.4    Tools/int_arith.ML \
     2.5    Tools/list_code.ML \
     2.6    Tools/list_to_set_comprehension.ML \
     2.7 +  Tools/monomorph.ML \
     2.8    Tools/nat_numeral_simprocs.ML \
     2.9    Tools/Nitpick/kodkod.ML \
    2.10    Tools/Nitpick/kodkod_sat.ML \