equal
deleted
inserted
replaced
506 \end{matharray} |
506 \end{matharray} |
507 The $name$ may be even omitted, although this would make it difficult to |
507 The $name$ may be even omitted, although this would make it difficult to |
508 declare the theorem otherwise later (e.g.\ as $[simp~del]$). |
508 declare the theorem otherwise later (e.g.\ as $[simp~del]$). |
509 |
509 |
510 |
510 |
511 \section{Converting to actual Isar proof texts} |
511 \section{Writing actual Isar proof texts} |
512 |
512 |
513 Porting legacy ML proof scripts into Isar tactic emulation scripts (see |
513 Porting legacy ML proof scripts into Isar tactic emulation scripts (see |
514 \S\ref{sec:port-scripts}) is mainly a technical issue, since the basic |
514 \S\ref{sec:port-scripts}) is mainly a technical issue, since the basic |
515 representation of formal ``proof script'' is preserved. In contrast, |
515 representation of formal ``proof script'' is preserved. In contrast, |
516 converting existing Isabelle developments into actual human-readably Isar |
516 converting existing Isabelle developments into actual human-readably Isar |