equal
deleted
inserted
replaced
519 For the functions @{text "assume"}, @{text "forall_elim"} etc |
519 For the functions @{text "assume"}, @{text "forall_elim"} etc |
520 see \isccite{sec:thms}. The basic functions for theorems are defined in |
520 see \isccite{sec:thms}. The basic functions for theorems are defined in |
521 @{ML_file "Pure/thm.ML"}. |
521 @{ML_file "Pure/thm.ML"}. |
522 \end{readmore} |
522 \end{readmore} |
523 |
523 |
|
524 (FIXME: how to add case-names to goal states) |
524 *} |
525 *} |
525 |
526 |
526 section {* Theories and Local Theories *} |
527 section {* Theories and Local Theories *} |
527 |
528 |
528 section {* Storing Theorems *} |
529 section {* Storing Theorems *} |