# HG changeset patch # User wenzelm # Date 862327433 -7200 # Node ID 4d501db6ebed2745ac935b2196d3839854a17c7d # Parent 3c548f92e032703a9f18a633857ee389115583eb renamed \ to \; diff -r 3c548f92e032 -r 4d501db6ebed lib/encodings/isabelle-0 --- a/lib/encodings/isabelle-0 Tue Apr 29 17:14:06 1997 +0200 +++ b/lib/encodings/isabelle-0 Tue Apr 29 17:23:53 1997 +0200 @@ -13,7 +13,7 @@ tturnstile langle rangle -choice +orelse top Or ocdot diff -r 3c548f92e032 -r 4d501db6ebed lib/scripts/symbolinput.pl --- a/lib/scripts/symbolinput.pl Tue Apr 29 17:14:06 1997 +0200 +++ b/lib/scripts/symbolinput.pl Tue Apr 29 17:23:53 1997 +0200 @@ -13,7 +13,7 @@ "\x95", "\\", "\x96", "\\", "\x97", "\\", - "\x98", "\\", + "\x98", "\\", "\x99", "\\", "\x9a", "\\", "\x9b", "\\", diff -r 3c548f92e032 -r 4d501db6ebed src/Pure/Syntax/symbol_font.ML --- a/src/Pure/Syntax/symbol_font.ML Tue Apr 29 17:14:06 1997 +0200 +++ b/src/Pure/Syntax/symbol_font.ML Tue Apr 29 17:23:53 1997 +0200 @@ -39,7 +39,7 @@ "tturnstile", "langle", "rangle", - "choice", + "orelse", "top", "Or", "ocdot",