| Tue, 27 Mar 2007 17:57:42 +0200 | berghofe | Adapted to new syntax of nominal_inductive. | changeset | files |
| Tue, 27 Mar 2007 17:57:05 +0200 | berghofe | Adapted to changes in nominal_inductive. | changeset | files |
| Tue, 27 Mar 2007 17:55:09 +0200 | berghofe | Implemented proof of strong induction rule. | changeset | files |
| Tue, 27 Mar 2007 17:54:37 +0200 | berghofe | Exported perm_of_pair, mk_not_sym, and perm_simproc. | changeset | files |
| Tue, 27 Mar 2007 12:28:42 +0200 | haftmann | cleaned up HOL/ex/Code*.thy | changeset | files |
| Tue, 27 Mar 2007 09:19:37 +0200 | haftmann | fixed document preparation | changeset | files |
| Mon, 26 Mar 2007 16:35:33 +0200 | krauss | fixed problem with mutual recursion | changeset | files |
| Mon, 26 Mar 2007 14:54:45 +0200 | haftmann | cleaned up Library/ and ex/ | changeset | files |
| Mon, 26 Mar 2007 14:53:07 +0200 | haftmann | minimal intro rules | changeset | files |
| Mon, 26 Mar 2007 14:53:06 +0200 | haftmann | exported interface for intro rules | changeset | files |
| Mon, 26 Mar 2007 14:53:05 +0200 | haftmann | moved Eval theory to library | changeset | files |
| Mon, 26 Mar 2007 14:53:04 +0200 | haftmann | Eval theory | changeset | files |
| Mon, 26 Mar 2007 14:53:03 +0200 | haftmann | tuned | changeset | files |
| Mon, 26 Mar 2007 14:53:02 +0200 | haftmann | importing Eval theory | changeset | files |
| Mon, 26 Mar 2007 14:53:01 +0200 | haftmann | naming tuned | changeset | files |
| Mon, 26 Mar 2007 14:53:00 +0200 | haftmann | cleaned up Library( and ex/ | changeset | files |
| Mon, 26 Mar 2007 12:48:30 +0200 | paulson | Clause cache is now in theory data. | changeset | files |
| Mon, 26 Mar 2007 12:46:27 +0200 | paulson | "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers. | changeset | files |
| Sun, 25 Mar 2007 15:15:07 +0200 | urbanc | moving lemmas into appropriate sections | changeset | files |
| Fri, 23 Mar 2007 12:06:41 +0100 | haftmann | fixed typing bug in generated code | changeset | files |
| Fri, 23 Mar 2007 12:05:43 +0100 | haftmann | fixed typing bug in generated code | changeset | files |
| Fri, 23 Mar 2007 10:50:03 +0100 | urbanc | added the permutation operation on options to the list of equivariance lemmas | changeset | files |
| Fri, 23 Mar 2007 09:46:22 +0100 | haftmann | dropped | changeset | files |
| Fri, 23 Mar 2007 09:40:57 +0100 | haftmann | added empty cases | changeset | files |
| Fri, 23 Mar 2007 09:40:53 +0100 | haftmann | added concept for term constructors | changeset | files |
| Fri, 23 Mar 2007 09:40:50 +0100 | haftmann | tuned | changeset | files |
| Fri, 23 Mar 2007 09:40:49 +0100 | haftmann | two further properties about lists | changeset | files |
| Fri, 23 Mar 2007 09:40:47 +0100 | haftmann | removed outdated example | changeset | files |
| Fri, 23 Mar 2007 09:40:45 +0100 | haftmann | fixed typo | changeset | files |
| Fri, 23 Mar 2007 09:40:43 +0100 | haftmann | added some sketches about library functions | changeset | files |