| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
mizar-insert-skeleton
You can use this feature to automatically create the basic skeleton proof steps for a proof of any formula.
If not nil, skeleton steps produced by ‘mizar-insert-skeleton’ are labeled.
The labels are created by concatenating the value of
‘mizar-default-label-name’ with a label number, which increases throughout
the skeleton from its initial value.
The non nil values of this variable determine the initial default as follows
'serial is used for starting from the last skeleton label number + 1 (default),
'constant-one always starts from 1,
'constant-zero always starts from 0.
The default value is serial.
Default name of labels inserted when ‘mizar-skeleton-labels’ is set.
This is appended with a label number.
The default value is "Z".
The function creating assumption skeletons out of a parsed formula.
See ‘mizar-default-assume-items’ for an example.
This function is called for creating assumptions in the function
‘mizar-default-skeleton-items’.
The default value is mizar-default-assume-items.
The function creating proof skeletons out of a parsed formula.
See ‘mizar-default-skeleton-items’ for an example.
This function is called in the interactive function
‘mizar-insert-skeleton’.
The default value is mizar-default-skeleton-items.
Insert a proof skeleton for the formula starting at beg after point end.
If ‘mizar-skeleton-labels’ is set, prompt additionally for the
first starting label number label-number, which should be an
integer. The labels are then generated using
‘mizar-default-label-name’.
For this command to work properly, the lisppars utility needs to be installed (which probably is the case, since lisppars has been distributed with Mizar since version 6.4), and the Mizar parser must be able to access the formula contained within the region delimited by beg and end (thus, it must not be within the scope of a comment).
This command calls ‘mizar-parse-region-fla’ to parse the formula
in the region delimiated by beg and end. It then creates the
desired skeleton by first using ‘mizar-skeleton-items-func’, and
then, for pretty printing, by using ‘mizar-skeleton-string’.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.