X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fgrafite.hrc;h=7ebf82f638dd967f2d0a0ec493192d02ca439b67;hb=0692f9fb99211c02a93c72d58c9177f9f994e4d9;hp=4b88fa91dc6b2f5707b918abbf77acc75f95f5e3;hpb=228d207d77101f153312e1c2cef1b8f2b5ec329f;p=helm.git
diff --git a/helm/www/matita/grafite.hrc b/helm/www/matita/grafite.hrc
index 4b88fa91d..7ebf82f63 100644
--- a/helm/www/matita/grafite.hrc
+++ b/helm/www/matita/grafite.hrc
@@ -1,188 +1,179 @@
-
-
-
- \
-
-
- \(\*\*[^\)]
- [^\(]\*\*\)
-
-
-
- \(\*
- \*\)
-
-
-
- theorem
- definition
- lemma
- fact
- remark
- variant
- axiom
-
-
-
- alias
- and
- as
- coercion
- coinductive
- corec
- default
- for
- include
- include'
- inductive
- in
- interpretation
- let
- match
- names
- notation
- on
- qed
- rec
- record
- return
- to
- using
- with
-
-
-
- \[
-
-
- \|
-
-
- \]
-
-
- \{
-
-
- \}
-
-
- @
-
-
- \$
-
-
-
- Set
- Prop
- Type
-
-
-
- absurd
- apply
- assumption
- auto
- paramodulation
- clear
- clearbody
- change
- constructor
- contradiction
- cut
- decompose
- discriminate
- elim
- elimType
- exact
- exists
- fail
- fold
- fourier
- fwd
- generalize
- goal
- id
- injection
- intro
- intros
- inversion
- lapply
- linear
- left
- letin
- normalize
- reduce
- reflexivity
- replace
- rewrite
- ring
- right
- symmetry
- simplify
- split
- to
- transitivity
- unfold
- whd
-
-
-
- try
- solve
- do
- repeat
- first
- focus
- unfocus
-
-
-
-
- check
- hint
- set
-
-
-
- elim
- hint
- instance
- locate
- match
-
-
-
- def
- forall
- lambda
- to
- exists
- Rightarrow
- Assign
- land
- lor
- lnot
- liff
- subst
- vdash
- iforall
- iexists
-
-
-
- "
- "
-
-
-
+
+
+
+
+
+
+
+ Grafite: Matita scripts language
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+