src/HOL/ex/svc_test.thy
changeset 17416 5093a587da16
parent 17388 495c799df31d
child 20807 bd3b60f9a343
equal deleted inserted replaced
17415:ec859c451f59 17416:5093a587da16
     6 theory svc_test
     6 theory svc_test
     7 imports SVC_Oracle
     7 imports SVC_Oracle
     8 begin
     8 begin
     9 
     9 
    10 syntax
    10 syntax
    11     "<->"         :: [bool, bool] => bool                  (infixr 25)
    11   "<->" :: "[bool, bool] => bool"    (infixr 25)
    12 
    12 
    13 translations
    13 translations
    14   "x <-> y" => "x = y"
    14   "x <-> y" => "x = y"
    15 
    15 
    16 end
    16 end