src/HOL/ex/svc_test.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17416 5093a587da16
child 20807 bd3b60f9a343
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 
     2 (* $Id$ *)
     3 
     4 header {* Demonstrating the interface SVC *}
     5 
     6 theory svc_test
     7 imports SVC_Oracle
     8 begin
     9 
    10 syntax
    11   "<->" :: "[bool, bool] => bool"    (infixr 25)
    12 
    13 translations
    14   "x <-> y" => "x = y"
    15 
    16 end