equal
deleted
inserted
replaced
448 fit into the traditional document model of "definition-statement-proof" |
448 fit into the traditional document model of "definition-statement-proof" |
449 via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. |
449 via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. |
450 |
450 |
451 |
451 |
452 *** HOL *** |
452 *** HOL *** |
|
453 |
|
454 * Simproc 'datatype_no_proper_subterm' rewrites equalities 'lhs = rhs' |
|
455 on datatypes to 'False' if either side is a proper subexpression of the |
|
456 other (for any datatype with a reasonable size function). |
453 |
457 |
454 * Command 'export_code' produces output as logical files within the |
458 * Command 'export_code' produces output as logical files within the |
455 theory context, as well as formal session exports that can be |
459 theory context, as well as formal session exports that can be |
456 materialized via command-line tools "isabelle export" or "isabelle build |
460 materialized via command-line tools "isabelle export" or "isabelle build |
457 -e" (with 'export_files' in the session ROOT). Isabelle/jEdit also |
461 -e" (with 'export_files' in the session ROOT). Isabelle/jEdit also |