--- 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
--- 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";
--- /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