load lambda-lifting structure earlier, so it can be used in Metis
authorblanchet
Tue Aug 09 09:05:21 2011 +0200 (2011-08-09)
changeset 440878e491cb8841c
parent 44086 c0847967a25a
child 44088 3693baa6befb
load lambda-lifting structure earlier, so it can be used in Metis
src/HOL/ATP.thy
src/HOL/IsaMakefile
src/HOL/SMT.thy
     1.1 --- a/src/HOL/ATP.thy	Tue Aug 09 07:44:17 2011 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue Aug 09 09:05:21 2011 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  theory ATP
     1.6  imports Meson
     1.7 -uses "Tools/monomorph.ML"
     1.8 +uses "Tools/lambda_lifting.ML"
     1.9 +     "Tools/monomorph.ML"
    1.10       "Tools/ATP/atp_util.ML"
    1.11       "Tools/ATP/atp_problem.ML"
    1.12       "Tools/ATP/atp_proof.ML"
     2.1 --- a/src/HOL/IsaMakefile	Tue Aug 09 07:44:17 2011 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Aug 09 09:05:21 2011 +0200
     2.3 @@ -244,7 +244,9 @@
     2.4    Tools/inductive_codegen.ML \
     2.5    Tools/inductive_realizer.ML \
     2.6    Tools/inductive_set.ML \
     2.7 +  Tools/lambda_lifting.ML \
     2.8    Tools/lin_arith.ML \
     2.9 +  Tools/monomorph.ML \
    2.10    Tools/nat_arith.ML \
    2.11    Tools/primrec.ML \
    2.12    Tools/prop_logic.ML \
    2.13 @@ -309,10 +311,8 @@
    2.14    Tools/code_evaluation.ML \
    2.15    Tools/groebner.ML \
    2.16    Tools/int_arith.ML \
    2.17 -  Tools/lambda_lifting.ML \
    2.18    Tools/list_code.ML \
    2.19    Tools/list_to_set_comprehension.ML \
    2.20 -  Tools/monomorph.ML \
    2.21    Tools/nat_numeral_simprocs.ML \
    2.22    Tools/Nitpick/kodkod.ML \
    2.23    Tools/Nitpick/kodkod_sat.ML \
     3.1 --- a/src/HOL/SMT.thy	Tue Aug 09 07:44:17 2011 +0200
     3.2 +++ b/src/HOL/SMT.thy	Tue Aug 09 09:05:21 2011 +0200
     3.3 @@ -7,7 +7,6 @@
     3.4  theory SMT
     3.5  imports Record
     3.6  uses
     3.7 -  "Tools/lambda_lifting.ML"
     3.8    "Tools/SMT/smt_utils.ML"
     3.9    "Tools/SMT/smt_failure.ML"
    3.10    "Tools/SMT/smt_config.ML"