X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_elimType.html;h=95be7857852c30867802d27786a8776f93f223c2;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=0381aeea48a807e54b576fd10403fded885dee44;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_elimType.html b/helm/www/matita/docs/manual/tac_elimType.html index 0381aeea4..95be78578 100644 --- a/helm/www/matita/docs/manual/tac_elimType.html +++ b/helm/www/matita/docs/manual/tac_elimType.html @@ -1,5 +1,5 @@ -elimType sterm [using sterm] [<intros_spec>]
elimType sterm [using sterm] [<intros_spec>]
Prev Chapter 6. Tactics Next

elimType sterm [using sterm] [<intros_spec>]

elimType T using th hyps

+elimType sterm [using sterm] [<intros_spec>]

elimType sterm [using sterm] [<intros_spec>]
Prev Chapter 6. Tactics Next

elimType sterm [using sterm] [<intros_spec>]

elimType T using th hyps

Pre-conditions:

T must be an inductive type.

Action:

TODO (severely bugged now).

New sequents to prove:

TODO

Prev Up Next
elim sterm [using sterm] [<intros_spec>] Home exact sterm