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
theorem
record
definition
inductive
coinductive
let
lemma
remark
axiom
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
discriminator
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
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]
∀|∃|λ|=|→|⇒|…|≝|≡|\?
\[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|:|-