added new print_mode "xsymbols" for extended symbol support
authoroheimb
Fri Dec 11 18:56:30 1998 +0100 (1998-12-11)
changeset 60279dd06eeda95c
parent 6026 649b98cf9bc3
child 6028 1bfd52528bde
added new print_mode "xsymbols" for extended symbol support
(e.g. genuiely long arrows)
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/Pure/Syntax/mixfix.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/FOL/IFOL.thy	Fri Dec 11 17:16:23 1998 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Fri Dec 11 18:56:30 1998 +0100
     1.3 @@ -63,6 +63,9 @@
     1.4    "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
     1.5    "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
     1.9 +  "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
    1.10  
    1.11  local
    1.12  
     2.1 --- a/src/HOL/HOL.thy	Fri Dec 11 17:16:23 1998 +0100
     2.2 +++ b/src/HOL/HOL.thy	Fri Dec 11 18:56:30 1998 +0100
     2.3 @@ -141,6 +141,8 @@
     2.4    "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
     2.5  
     2.6  
     2.7 +syntax (xsymbols)
     2.8 +  "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
     2.9  
    2.10  (** Rules and definitions **)
    2.11  
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Dec 11 17:16:23 1998 +0100
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 11 18:56:30 1998 +0100
     3.3 @@ -30,7 +30,8 @@
     3.4    val pure_syntax: (string * string * mixfix) list
     3.5    val pure_appl_syntax: (string * string * mixfix) list
     3.6    val pure_applC_syntax: (string * string * mixfix) list
     3.7 -  val pure_sym_syntax: (string * string * mixfix) list
     3.8 +  val pure_sym_syntax:  (string * string * mixfix) list
     3.9 +  val pure_xsym_syntax: (string * string * mixfix) list
    3.10  end;
    3.11  
    3.12  signature MIXFIX =
    3.13 @@ -220,5 +221,8 @@
    3.14    ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
    3.15    ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
    3.16  
    3.17 +val pure_xsym_syntax =
    3.18 + [("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
    3.19 +  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1))];
    3.20  
    3.21  end;
     4.1 --- a/src/Pure/pure_thy.ML	Fri Dec 11 17:16:23 1998 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Fri Dec 11 18:56:30 1998 +0100
     4.3 @@ -425,7 +425,8 @@
     4.4      ("itself", [logicS], logicS)]
     4.5    |> Theory.add_nonterminals Syntax.pure_nonterms
     4.6    |> Theory.add_syntax Syntax.pure_syntax
     4.7 -  |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
     4.8 +  |> Theory.add_modesyntax ("symbols" , true) Syntax.pure_sym_syntax
     4.9 +  |> Theory.add_modesyntax ("xsymbols", true) Syntax.pure_xsym_syntax
    4.10    |> Theory.add_trfuns Syntax.pure_trfuns
    4.11    |> Theory.add_trfunsT Syntax.pure_trfunsT
    4.12    |> Theory.add_syntax