On Thu, 7 Oct 2010, Lukas Bulwahn wrote:
The code_pred command for the invocation of the predicate compiler could
also fit under this umbrella.
So the syntax would change from "code_pred" to "prove code_pred" which
is actually better, because then users are not surprised that the
command sets up some goal state (in most cases the empty goal) for the
user to prove.
This scheme would be outside of Isar traditions for several reasons, such
as the naming of toplevel commands (nouns, not verbs).
BTW, the very idea of an empty goal state shown to the user belongs to the
PG interaction model. It is easy to imagine an Isar prover IDE that fills
such holes seemlessly according to the formal structure of the text. The
traditional mismatch of PG interaction and Isar structure may soon be
overcome in the new document model.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
