X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fmatita.lang;h=be110b9baab536a4a2d7b2665b152b3a63845e69;hb=c74a1a8237c8a05d26be0112f560d24de8cd9f0f;hp=9238684a08cc4de408bd86aef9bfeb85bbee2bb5;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git
diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index 9238684a0..be110b9ba 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,122 +74,35 @@
+
theorem
+ record
definition
+ inductive
+ coinductive
+ let
lemma
- fact
remark
- variant
axiom
-
- ntheorem
- nrecord
- ndefinition
- ninductive
- ncoinductive
- nlet
- nlemma
- nremark
- naxiom
-
- 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
+ apply
+ applyS
+ cases
+ letin
+ auto
+ elim
+ whd
+ normalize
+ assumption
+ generalize
+ change
+ rewrite
+ cut
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
-
-
- napply
- napplyS
- ncases
- nletin
- nauto
- nelim
- nwhd
- nnormalize
- nassumption
- ngeneralize
- nchange
- nrewrite
- ncut
- ninversion
- nlapply
- ndestruct
+ destruct
alias
@@ -209,6 +114,7 @@
coinductive
corec
default
+ discriminator
for
include
include'
@@ -231,16 +137,14 @@
with
-
+
unification
hint
- ncoercion
- ninverter
- nqed
+ coercion
+ inverter
+ qed
- inline
- procedural
check
eval
hint
@@ -250,10 +154,6 @@
coercions
comments
debug
- cr
-
-
- ncheck
try
@@ -268,12 +168,6 @@
- Set
- Prop
- Type
- CProp
-
-
Prop
Type[0]
CProp[0]
@@ -287,7 +181,7 @@
â|â|λ|=|â|â|â¦|â|â¡|\?
- \[|\||\]|\{|\}|@|\$|#|\\\\|;|\.|:>|:
+ \[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|:|-