deactivated new symbols (not yet printable on xterm, emacs);
authorwenzelm
Tue Apr 29 17:38:02 1997 +0200 (1997-04-29)
changeset 3068b7562e452816
parent 3067 4d501db6ebed
child 3069 de1f64558c01
deactivated new symbols (not yet printable on xterm, emacs);
lib/encodings/isabelle-0
lib/scripts/symbolinput.pl
src/HOL/HOL.thy
src/Pure/Syntax/symbol_font.ML
src/ZF/ZF.thy
     1.1 --- a/lib/encodings/isabelle-0	Tue Apr 29 17:23:53 1997 +0200
     1.2 +++ b/lib/encodings/isabelle-0	Tue Apr 29 17:38:02 1997 +0200
     1.3 @@ -4,23 +4,26 @@
     1.4  # The isabelle-0 encoding table.
     1.5  #
     1.6  
     1.7 -145:
     1.8 +#145:
     1.9 +#
    1.10 +#lless
    1.11 +#unlhd
    1.12 +#lhd
    1.13 +#rhd
    1.14 +#tturnstile
    1.15 +#langle
    1.16 +#rangle
    1.17 +#orelse
    1.18 +#top
    1.19 +#Or
    1.20 +#ocdot
    1.21 +#iota
    1.22 +#upsilon
    1.23 +#Upsilon
    1.24 +#Xi
    1.25  
    1.26 -lless
    1.27 -unlhd
    1.28 -lhd
    1.29 -rhd
    1.30 -tturnstile
    1.31 -langle
    1.32 -rangle
    1.33 -orelse
    1.34 -top
    1.35 -Or
    1.36 -ocdot
    1.37 -iota
    1.38 -upsilon
    1.39 -Upsilon
    1.40 -Xi
    1.41 +160:
    1.42 +
    1.43  space2
    1.44  Gamma
    1.45  Delta
     2.1 --- a/lib/scripts/symbolinput.pl	Tue Apr 29 17:23:53 1997 +0200
     2.2 +++ b/lib/scripts/symbolinput.pl	Tue Apr 29 17:38:02 1997 +0200
     2.3 @@ -6,21 +6,6 @@
     2.4  
     2.5  %tab = (
     2.6  #GENERATED TEXT FOLLOWS - Do not edit!
     2.7 -  "\x91", "\\<lless>",
     2.8 -  "\x92", "\\<unlhd>",
     2.9 -  "\x93", "\\<lhd>",
    2.10 -  "\x94", "\\<rhd>",
    2.11 -  "\x95", "\\<tturnstile>",
    2.12 -  "\x96", "\\<langle>",
    2.13 -  "\x97", "\\<rangle>",
    2.14 -  "\x98", "\\<orelse>",
    2.15 -  "\x99", "\\<top>",
    2.16 -  "\x9a", "\\<Or>",
    2.17 -  "\x9b", "\\<ocdot>",
    2.18 -  "\x9c", "\\<iota>",
    2.19 -  "\x9d", "\\<upsilon>",
    2.20 -  "\x9e", "\\<Upsilon>",
    2.21 -  "\x9f", "\\<Xi>",
    2.22    "\xa0", "\\<space2>",
    2.23    "\xa1", "\\<Gamma>",
    2.24    "\xa2", "\\<Delta>",
     3.1 --- a/src/HOL/HOL.thy	Tue Apr 29 17:23:53 1997 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Apr 29 17:38:02 1997 +0200
     3.3 @@ -123,7 +123,7 @@
     3.4    "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
     3.5    "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
     3.6    "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
     3.7 -  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")
     3.8 +(*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
     3.9  
    3.10  syntax (symbols output)
    3.11    "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
     4.1 --- a/src/Pure/Syntax/symbol_font.ML	Tue Apr 29 17:23:53 1997 +0200
     4.2 +++ b/src/Pure/Syntax/symbol_font.ML	Tue Apr 29 17:38:02 1997 +0200
     4.3 @@ -26,27 +26,12 @@
     4.4  
     4.5  (* tables *)
     4.6  
     4.7 -val enc_start = 145;
     4.8 +val enc_start = 161;
     4.9  val enc_end = 255;
    4.10  
    4.11  val enc_vector =
    4.12  [
    4.13  (* GENERATED TEXT FOLLOWS - Do not edit! *)
    4.14 -  "lless",
    4.15 -  "unlhd",
    4.16 -  "lhd",
    4.17 -  "rhd",
    4.18 -  "tturnstile",
    4.19 -  "langle",
    4.20 -  "rangle",
    4.21 -  "orelse",
    4.22 -  "top",
    4.23 -  "Or",
    4.24 -  "ocdot",
    4.25 -  "iota",
    4.26 -  "upsilon",
    4.27 -  "Upsilon",
    4.28 -  "Xi",
    4.29    "space2",
    4.30    "Gamma",
    4.31    "Delta",
     5.1 --- a/src/ZF/ZF.thy	Tue Apr 29 17:23:53 1997 +0200
     5.2 +++ b/src/ZF/ZF.thy	Tue Apr 29 17:38:02 1997 +0200
     5.3 @@ -149,8 +149,10 @@
     5.4    "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma> _\\<in>_./ _)" 10)
     5.5    "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall> _\\<in>_./ _)" 10)
     5.6    "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
     5.7 +(*
     5.8    "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
     5.9    "@pttrn"    :: pttrns => pttrn           ("\\<langle>_\\<rangle>")
    5.10 +*)
    5.11  
    5.12  
    5.13  defs