text/x-matita
*.ma
(*
*)
\\"|[0-9a-zA-Z]
\%{char-esc}
"
"
('\%{char-esc}')|('[^\\']')
\\
def
forall
lambda
to
exists
Rightarrow
Assign
land
lor
lnot
liff
subst
vdash
iforall
iexists
implied
theorem
record
definition
inductive
coinductive
fact
lemma
remark
axiom
apply
applyS
cases
letin
auto
elim
whd
normalize
assumption
generalize
change
rewrite
cut
inversion
lapply
destruct
assume
suppose
that
is
equivalent
to
we
need
prove
or
equivalently
by
done
proved
have
such
the
thesis
becomes
conclude
obtain
proceed
induction
case
hypothesis
know
alias
and
as
associative
coercion
prefer
nocomposites
coinductive
constraint
corec
cyclic
default
discriminator
for
id
include
include'
inductive
inverter
in
interpretation
left
let
match
names
non
notation
on
precedence
qed
defined
rec
record
return
right
source
symbol
to
universe
using
with
unification
hint
coercion
inverter
qed
check
eval
hint
set
auto
nodefaults
coercions
comments
debug
try
solve
do
repeat
first
focus
unfocus
progress
skip
Prop
Type[0]
CProp[0]
Type[1]
CProp[1]
Type[2]
CProp[2]
∀|∃|λ|=|→|⇒|…|≝|≡|\?
\[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|:|-