#explode_widget
command #
Render a widget that displays an #explode
proof, providing more
interactivity such as jumping to definitions and exploding constants
occurring in the exploded proofs.
Redefine some of the style attributes for better formatting.
Explode button for subsequent exploding.
Render a subexpression as a list of html elements.
Component for the type tooltip.
Component that shows a type.
Component that shows a constant.
Search for an entry that has the specified line number.
Render a row that shows the ID of a goal.
Render a row that shows the rule or theorem being applied.
Render a row that contains the sub-proofs, i.e., the proofs of the arguments.
Combine the goal row, id row, rule row and proof row to make them a table.
Render a table for a given entry.
Render a widget from given entries.
Explode a theorem and return entries.
User command of the explode widget.