Thu, 19 Jul 2007 15:35:00 +0200 | berghofe | Refer to major premise of induction rule via "thm_style prem1". | changeset | files |
Thu, 19 Jul 2007 15:33:27 +0200 | berghofe | Added named_thms antiquotation. | changeset | files |
Thu, 19 Jul 2007 15:32:58 +0200 | berghofe | Replaced "hand-made" files by generated files in Inductive/document. | changeset | files |
Thu, 19 Jul 2007 15:31:30 +0200 | berghofe | LaTeX code is now generated directly from theory files. | changeset | files |
Thu, 19 Jul 2007 15:30:35 +0200 | berghofe | LaTeX code is now generated directly from Even and Advanced theories. | changeset | files |
Thu, 19 Jul 2007 15:29:51 +0200 | berghofe | LaTeX code is now generated directly from theory file. | changeset | files |