--- 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
--- 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>",
--- 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)
--- 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",
--- 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