# HG changeset patch
# User wenzelm
# Date 862328282 -7200
# Node ID b7562e4528168036fb159bc7884e4b36e73afa16
# Parent  4d501db6ebed2745ac935b2196d3839854a17c7d
deactivated new symbols (not yet printable on xterm, emacs);

diff -r 4d501db6ebed -r b7562e452816 lib/encodings/isabelle-0
--- a/lib/encodings/isabelle-0	Tue Apr 29 17:23:53 1997 +0200
+++ b/lib/encodings/isabelle-0	Tue Apr 29 17:38:02 1997 +0200
@@ -4,23 +4,26 @@
 # The isabelle-0 encoding table.
 #
 
-145:
+#145:
+#
+#lless
+#unlhd
+#lhd
+#rhd
+#tturnstile
+#langle
+#rangle
+#orelse
+#top
+#Or
+#ocdot
+#iota
+#upsilon
+#Upsilon
+#Xi
 
-lless
-unlhd
-lhd
-rhd
-tturnstile
-langle
-rangle
-orelse
-top
-Or
-ocdot
-iota
-upsilon
-Upsilon
-Xi
+160:
+
 space2
 Gamma
 Delta
diff -r 4d501db6ebed -r b7562e452816 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Tue Apr 29 17:23:53 1997 +0200
+++ b/lib/scripts/symbolinput.pl	Tue Apr 29 17:38:02 1997 +0200
@@ -6,21 +6,6 @@
 
 %tab = (
 #GENERATED TEXT FOLLOWS - Do not edit!
-  "\x91", "\\<lless>",
-  "\x92", "\\<unlhd>",
-  "\x93", "\\<lhd>",
-  "\x94", "\\<rhd>",
-  "\x95", "\\<tturnstile>",
-  "\x96", "\\<langle>",
-  "\x97", "\\<rangle>",
-  "\x98", "\\<orelse>",
-  "\x99", "\\<top>",
-  "\x9a", "\\<Or>",
-  "\x9b", "\\<ocdot>",
-  "\x9c", "\\<iota>",
-  "\x9d", "\\<upsilon>",
-  "\x9e", "\\<Upsilon>",
-  "\x9f", "\\<Xi>",
   "\xa0", "\\<space2>",
   "\xa1", "\\<Gamma>",
   "\xa2", "\\<Delta>",
diff -r 4d501db6ebed -r b7562e452816 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Apr 29 17:23:53 1997 +0200
+++ b/src/HOL/HOL.thy	Tue Apr 29 17:38:02 1997 +0200
@@ -123,7 +123,7 @@
   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
-  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")
+(*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
 
 syntax (symbols output)
   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
diff -r 4d501db6ebed -r b7562e452816 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Tue Apr 29 17:23:53 1997 +0200
+++ b/src/Pure/Syntax/symbol_font.ML	Tue Apr 29 17:38:02 1997 +0200
@@ -26,27 +26,12 @@
 
 (* tables *)
 
-val enc_start = 145;
+val enc_start = 161;
 val enc_end = 255;
 
 val enc_vector =
 [
 (* GENERATED TEXT FOLLOWS - Do not edit! *)
-  "lless",
-  "unlhd",
-  "lhd",
-  "rhd",
-  "tturnstile",
-  "langle",
-  "rangle",
-  "orelse",
-  "top",
-  "Or",
-  "ocdot",
-  "iota",
-  "upsilon",
-  "Upsilon",
-  "Xi",
   "space2",
   "Gamma",
   "Delta",
diff -r 4d501db6ebed -r b7562e452816 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Apr 29 17:23:53 1997 +0200
+++ b/src/ZF/ZF.thy	Tue Apr 29 17:38:02 1997 +0200
@@ -149,8 +149,10 @@
   "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma> _\\<in>_./ _)" 10)
   "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall> _\\<in>_./ _)" 10)
   "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
+(*
   "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
   "@pttrn"    :: pttrns => pttrn           ("\\<langle>_\\<rangle>")
+*)
 
 
 defs