Added file Tools/res_atpset.ML.
authormengj
Wed Mar 01 06:06:16 2006 +0100 (2006-03-01)
changeset 19161b395f586633f
parent 19160 c1b3aa0a6827
child 19162 67436e2a16df
Added file Tools/res_atpset.ML.
src/HOL/IsaMakefile
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 01 06:05:25 2006 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 01 06:06:16 2006 +0100
     1.3 @@ -77,6 +77,7 @@
     1.4    $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
     1.5    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
     1.6    $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
     1.7 +  Tools/res_atpset.ML \
     1.8    Binomial.thy Datatype.ML Datatype.thy			\
     1.9    Datatype_Universe.thy Divides.thy						\
    1.10    Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
     2.1 --- a/src/HOL/ROOT.ML	Wed Mar 01 06:05:25 2006 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Wed Mar 01 06:06:16 2006 +0100
     2.3 @@ -31,6 +31,9 @@
     2.4  use "~~/src/Provers/quasi.ML";
     2.5  use "~~/src/Provers/order.ML";
     2.6  
     2.7 +
     2.8 +use "Tools/res_atpset.ML";
     2.9 +
    2.10  with_path "Integ" use_thy "Main";
    2.11  
    2.12  path_add "~~/src/HOL/Library";