# HG changeset patch
# User paulson
# Date 933930320 -7200
# Node ID 35676093459dd73cb9b71634e4da7a6b5c852510
# Parent  6ffe5067d5cc4d44d3fd93b89f92bd705570e6ab
new theory ex/svc_test.thy

diff -r 6ffe5067d5cc -r 35676093459d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Aug 05 22:11:43 1999 +0200
+++ b/src/HOL/IsaMakefile	Fri Aug 06 11:05:20 1999 +0200
@@ -326,7 +326,7 @@
   ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
   ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
   ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
-  ex/BinEx.ML ex/BinEx.thy ex/svc_test.ML ex/MonoidGroup.thy \
+  ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \
   ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
   ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy
 	@$(ISATOOL) usedir $(OUT)/HOL ex
diff -r 6ffe5067d5cc -r 35676093459d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Aug 05 22:11:43 1999 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Aug 06 11:05:20 1999 +0200
@@ -33,7 +33,7 @@
 
 time_use_thy "StringEx";
 time_use_thy "BinEx";
-time_use     "svc_test.ML";
+time_use_thy "svc_test";
 
 (*basic use of extensible records*)
 time_use_thy "MonoidGroup";
diff -r 6ffe5067d5cc -r 35676093459d src/HOL/ex/svc_test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/svc_test.thy	Fri Aug 06 11:05:20 1999 +0200
@@ -0,0 +1,9 @@
+svc_test = Main +
+
+syntax
+    "<->"         :: [bool, bool] => bool                  (infixr 25)
+
+translations
+  "x <-> y" => "x = y"
+
+end