# HG changeset patch
# User wenzelm
# Date 1130414078 -7200
# Node ID 4379d46c8e136d05a2fda68749865c883db0b4a1
# Parent  ca0958ab32939fea67630090238ce506d0c30c5e
alternative iff syntax for equality on booleans, with print_mode 'iff';

diff -r ca0958ab3293 -r 4379d46c8e13 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 27 08:14:05 2005 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 27 13:54:38 2005 +0200
@@ -119,6 +119,22 @@
   "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
 
+syntax
+  "_iff" :: "bool => bool => bool"                       (infixr "<->" 25)
+syntax (xsymbols)
+  "_iff" :: "bool => bool => bool"                       (infixr "\<longleftrightarrow>" 25)
+translations
+  "op <->" => "op = :: bool => bool => bool"
+
+typed_print_translation {*
+  let
+    fun iff_tr' _ (Type ("fun", (Type ("bool", _) :: _))) ts =
+          if Output.has_mode "iff" then Term.list_comb (Syntax.const "_iff", ts)
+          else raise Match
+      | iff_tr' _ _ _ = raise Match;
+  in [("op =", iff_tr')] end
+*}
+
 
 subsubsection {* Axioms and basic definitions *}