13. Proof Skeletons

C-c s

mizar-insert-skeleton

You can use this feature to automatically create the basic skeleton proof steps for a proof of any formula.

User Option: mizar-skeleton-labels

If set, skeleton steps produced by `mizar-insert-skeleton' are labeled.

The default value is nil.

User Option: mizar-default-label-name

Default name of labels inserted when `mizar-skeleton-labels' is set.
This is appended with a label number.

The default value is "Z".

User Option: mizar-assume-items-func

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.

User Option: mizar-skeleton-items-func

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.

Command: mizar-insert-skeleton beg end &optional labnr

Insert a proof skeleton for formula starting at beg after point end.
For normal interactive usage, just select the region containing the formula, and run this function. If `mizar-skeleton-labels' is set, prompts additionaly for the first starting label number labnr. The labels are then generated using the `mizar-default-label-name' string. The lisppars utility needs to be installed for this to work - it is distributed with Mizar since version 6.4, and the formula has to be accessible in the article to the Mizar parser - e.g. not commented. Calls `mizar-parse-region-fla' to parse the formula, Then creates the skeleton using `mizar-skeleton-items-func', and pretty prints it using `mizar-skeleton-string'.