src/HOL/ex/svc_test.thy
changeset 17388 495c799df31d
parent 12873 d7f8dfaad46d
child 17416 5093a587da16
equal deleted inserted replaced
17387:40ce48cc45f7 17388:495c799df31d
     1 
     1 
     2 svc_test = SVC_Oracle +
     2 (* $Id$ *)
       
     3 
       
     4 header {* Demonstrating the interface SVC *}
       
     5 
       
     6 theory svc_test
       
     7 imports SVC_Oracle
       
     8 begin
     3 
     9 
     4 syntax
    10 syntax
     5     "<->"         :: [bool, bool] => bool                  (infixr 25)
    11     "<->"         :: [bool, bool] => bool                  (infixr 25)
     6 
    12 
     7 translations
    13 translations