text/x-matita
*.ma
(*
*)
\\"|[0-9a-zA-Z]
\%{char-esc}
"
"
('\%{char-esc}')|('[^\\']')
whelp *
elim
hint
instance
locate
match
\\
def
forall
lambda
to
exists
Rightarrow
Assign
land
lor
lnot
liff
subst
vdash
iforall
iexists
theorem
definition
lemma
fact
remark
variant
axiom
theorem
record
definition
inductive
coinductive
let
lemma
remark
axiom
absurd
apply
applyP
assumption
autobatch
cases
clear
clearbody
change
compose
constructor
contradiction
cut
decompose
destruct
elim
elimType
exact
exists
fail
fold
fourier
fwd
generalize
id
intro
intros
inversion
lapply
linear
left
letin
normalize
reflexivity
replace
rewrite
ring
right
symmetry
simplify
split
to
transitivity
unfold
whd
assume
suppose
by
is
or
equivalent
equivalently
we
prove
proved
need
proceed
induction
inductive
case
base
let
such
that
by
have
and
the
thesis
becomes
hypothesis
know
case
obtain
conclude
done
rule
apply
applyS
cases
letin
auto
elim
whd
normalize
assumption
generalize
change
rewrite
cut
inversion
lapply
destruct
alias
and
as
coercion
prefer
nocomposites
coinductive
corec
default
for
include
include'
inductive
inverter
in
interpretation
let
match
names
notation
on
qed
rec
record
return
source
to
using
with
unification
hint
coercion
inverter
qed
inline
procedural
check
eval
hint
set
auto
odefaults
coercions
comments
debug
cr
check
try
solve
do
repeat
first
focus
unfocus
progress
skip
Set
Prop
Type
CProp
Prop
Type[0]
CProp[0]
Type[1]
CProp[1]
Type[2]
CProp[2]
∀|∃|λ|=|→|⇒|…|≝|≡|\?
\[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|: