# HG changeset patch
# User paulson
# Date 933585841 -7200
# Node ID 89e0ff71d1136cdfb9639a6a561635d644c3374b
# Parent  a67dde8820c02eaff5be128a97e6e0fb1261c8f2
new files for the SVC link-up

diff -r a67dde8820c0 -r 89e0ff71d113 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jul 30 18:27:25 1999 +0200
+++ b/src/HOL/IsaMakefile	Mon Aug 02 11:24:01 1999 +0200
@@ -56,12 +56,14 @@
   Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
   Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
   Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
+  SVC_Oracle.ML SVC_Oracle.thy \
   Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
   Tools/datatype_package.ML Tools/datatype_prop.ML \
   Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
   Tools/inductive_package.ML Tools/numeral_syntax.ML \
   Tools/primrec_package.ML Tools/recdef_package.ML \
-  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
+  Tools/record_package.ML Tools/svc_funcs.ML \
+  Tools/typedef_package.ML Trancl.ML \
   Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
   WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
   hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
diff -r a67dde8820c0 -r 89e0ff71d113 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Jul 30 18:27:25 1999 +0200
+++ b/src/HOL/ROOT.ML	Mon Aug 02 11:24:01 1999 +0200
@@ -75,6 +75,9 @@
 use "bin_simprocs.ML";
 cd "..";
 
+use "Tools/svc_funcs.ML";
+use_thy "SVC_Oracle";
+
 (*the all-in-one theory*)
 use_thy "Main";