# HG changeset patch
# User paulson
# Date 933678954 -7200
# Node ID 8c937127fd8c5760fe9d4e88eb970b91ead58335
# Parent  295882e50b7a90f6bca54d47999d8114dafdc1f0
new examples file for SVC

diff -r 295882e50b7a -r 8c937127fd8c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Aug 03 13:15:36 1999 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Aug 03 13:15:54 1999 +0200
@@ -33,6 +33,7 @@
 
 time_use_thy "StringEx";
 time_use_thy "BinEx";
+time_use     "svc_test.ML";
 
 (*basic use of extensible records*)
 time_use_thy "MonoidGroup";