# HG changeset patch
# User oheimb
# Date 913398990 -3600
# Node ID 9dd06eeda95ccddc280f4ba82944a73284ae6b58
# Parent  649b98cf9bc3f7a1658232a0303f276188fe4f9e
added new print_mode "xsymbols" for extended symbol support
(e.g. genuiely long arrows)

diff -r 649b98cf9bc3 -r 9dd06eeda95c src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Dec 11 17:16:23 1998 +0100
+++ b/src/FOL/IFOL.thy	Fri Dec 11 18:56:30 1998 +0100
@@ -63,6 +63,9 @@
   "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
   "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
 
+syntax (xsymbols)
+  "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
+  "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
 
 local
 
diff -r 649b98cf9bc3 -r 9dd06eeda95c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Dec 11 17:16:23 1998 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 11 18:56:30 1998 +0100
@@ -141,6 +141,8 @@
   "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
 
 
+syntax (xsymbols)
+  "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
 
 (** Rules and definitions **)
 
diff -r 649b98cf9bc3 -r 9dd06eeda95c src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Dec 11 17:16:23 1998 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 11 18:56:30 1998 +0100
@@ -30,7 +30,8 @@
   val pure_syntax: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
   val pure_applC_syntax: (string * string * mixfix) list
-  val pure_sym_syntax: (string * string * mixfix) list
+  val pure_sym_syntax:  (string * string * mixfix) list
+  val pure_xsym_syntax: (string * string * mixfix) list
 end;
 
 signature MIXFIX =
@@ -220,5 +221,8 @@
   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
 
+val pure_xsym_syntax =
+ [("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
+  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1))];
 
 end;
diff -r 649b98cf9bc3 -r 9dd06eeda95c src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Dec 11 17:16:23 1998 +0100
+++ b/src/Pure/pure_thy.ML	Fri Dec 11 18:56:30 1998 +0100
@@ -425,7 +425,8 @@
     ("itself", [logicS], logicS)]
   |> Theory.add_nonterminals Syntax.pure_nonterms
   |> Theory.add_syntax Syntax.pure_syntax
-  |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
+  |> Theory.add_modesyntax ("symbols" , true) Syntax.pure_sym_syntax
+  |> Theory.add_modesyntax ("xsymbols", true) Syntax.pure_xsym_syntax
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Theory.add_syntax