eliminated Syntax.binding;
put_thms: ignore "";
update_binds_env: Envir.norm_term ensures proper type instantiation;
#
# $Id$
#
# The isabelle-0 encoding table.
#
#145:
#
#lless
#unlhd
#lhd
#rhd
#tturnstile
#langle
#rangle
#orelse
#top
#Or
#ocdot
#iota
#upsilon
#Upsilon
#Xi
160:
spacespace
Gamma
Delta
Theta
Lambda
Pi
Sigma
Phi
Psi
Omega
alpha
beta
gamma
delta
epsilon
zeta
eta
theta
kappa
lambda
mu
nu
xi
pi
rho
sigma
tau
phi
chi
psi
omega
not
and
or
forall
exists
And
lceil
rceil
lfloor
rfloor
turnstile
Turnstile
lbrakk
rbrakk
cdot
in
subseteq
inter
union
Inter
Union
sqinter
squnion
Sqinter
Squnion
bottom
doteq
equiv
noteq
sqsubset
sqsubseteq
prec
preceq
succ
approx
sim
simeq
le
Colon
leftarrow
midarrow
rightarrow
Leftarrow
Midarrow
Rightarrow
bow
mapsto
leadsto
up
down
notin
times
oplus
ominus
otimes
oslash
subset
infinity
box
diamond
circ
bullet
parallel
surd
copyright