src/HOL/ex/svc_test.thy

--- a/src/HOL/ex/svc_test.thy	Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/svc_test.thy	Wed Sep 14 22:08:08 2005 +0200
@@ -1,5 +1,11 @@
 
-svc_test = SVC_Oracle +
+(* $Id$ *)
+
+header {* Demonstrating the interface SVC *}
+
+theory svc_test
+imports SVC_Oracle
+begin
 
 syntax
     "<->"         :: [bool, bool] => bool                  (infixr 25)