X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fmatita.lang;h=56cb0c41149c3db6a6d3956924df7813415cb421;hb=8db3579bec4d9a97af526f95a179587a2fbfe3e3;hp=bbfcb4ff2487543ddffc199fd77dac18c6d1a925;hpb=b72ec5a3af4c5fd7be09584afb31dd3f0cea3173;p=helm.git
diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index bbfcb4ff2..56cb0c411 100644
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -54,14 +54,6 @@
('\%{char-esc}')|('[^\\']')
-
- whelp *
- elim
- hint
- instance
- locate
- match
-
\\
def
@@ -82,156 +74,110 @@
-
- theorem
- definition
- lemma
- fact
- remark
- variant
- axiom
-
+
+ implied
+
+
theorem
record
definition
inductive
coinductive
- let
- lemma
+ fact
+ lemma
remark
axiom
- absurd
apply
- applyP
- assumption
- autobatch
+ applyS
cases
- clear
- clearbody
- change
- compose
- constructor
- contradiction
- cut
- decompose
- destruct
+ letin
+ auto
elim
- elimType
- exact
- exists
- fail
- fold
- fourier
- fwd
+ whd
+ normalize
+ assumption
generalize
- id
- intro
- intros
+ change
+ rewrite
+ cut
inversion
lapply
- linear
- left
- letin
- normalize
- reflexivity
- replace
- rewrite
- ring
- right
- symmetry
- simplify
- split
- to
- transitivity
- unfold
- whd
+ destruct
assume
suppose
- by
+ that
is
- or
equivalent
- equivalently
+ to
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
+ 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
- notation
+ non
+ notation
on
+ precedence
qed
+ defined
rec
record
return
- source
+ right
+ source
+ symbol
to
- using
+ universe
+ using
with
-
-
-
+
+
+
unification
hint
coercion
@@ -239,22 +185,16 @@
qed
- inline
- procedural
check
eval
hint
set
auto
- odefaults
+ nodefaults
coercions
comments
debug
- cr
-
-
- check
-
+
try
solve
@@ -268,12 +208,6 @@
- Set
- Prop
- Type
- CProp
-
-
Prop
Type[0]
CProp[0]
@@ -287,7 +221,7 @@
â|â|λ|=|â|â|â¦|â|â¡|\?
- \[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|:
+ \[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|:|-