new files for the SVC link-up
authorpaulson
Mon Aug 02 11:24:01 1999 +0200 (1999-08-02)
changeset 714289e0ff71d113
parent 7141 a67dde8820c0
child 7143 9c02848c5404
new files for the SVC link-up
src/HOL/IsaMakefile
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jul 30 18:27:25 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 02 11:24:01 1999 +0200
     1.3 @@ -56,12 +56,14 @@
     1.4    Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
     1.5    Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
     1.6    Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
     1.7 +  SVC_Oracle.ML SVC_Oracle.thy \
     1.8    Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
     1.9    Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.10    Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    1.11    Tools/inductive_package.ML Tools/numeral_syntax.ML \
    1.12    Tools/primrec_package.ML Tools/recdef_package.ML \
    1.13 -  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
    1.14 +  Tools/record_package.ML Tools/svc_funcs.ML \
    1.15 +  Tools/typedef_package.ML Trancl.ML \
    1.16    Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    1.17    WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    1.18    hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
     2.1 --- a/src/HOL/ROOT.ML	Fri Jul 30 18:27:25 1999 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Mon Aug 02 11:24:01 1999 +0200
     2.3 @@ -75,6 +75,9 @@
     2.4  use "bin_simprocs.ML";
     2.5  cd "..";
     2.6  
     2.7 +use "Tools/svc_funcs.ML";
     2.8 +use_thy "SVC_Oracle";
     2.9 +
    2.10  (*the all-in-one theory*)
    2.11  use_thy "Main";
    2.12