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
wenzelm@12873
     1
wenzelm@17388
     2
(* $Id$ *)
wenzelm@17388
     3
wenzelm@17388
     4
header {* Demonstrating the interface SVC *}
wenzelm@17388
     5
wenzelm@17388
     6
theory svc_test
wenzelm@17388
     7
imports SVC_Oracle
wenzelm@17388
     8
begin
paulson@7180
     9
paulson@7180
    10
syntax
wenzelm@17416
    11
  "<->" :: "[bool, bool] => bool"    (infixr 25)
paulson@7180
    12
paulson@7180
    13
translations
paulson@7180
    14
  "x <-> y" => "x = y"
paulson@7180
    15
paulson@7180
    16
end