| Tue, 03 Jul 2007 22:27:05 +0200 | wenzelm | use hologic.ML in basic HOL context; | file | diff | annotate |
| Tue, 03 Jul 2007 17:17:04 +0200 | wenzelm | CONVERSION tactical; | file | diff | annotate |
| Thu, 28 Jun 2007 19:09:32 +0200 | haftmann | simplified keyword setup | file | diff | annotate |
| Sun, 17 Jun 2007 13:39:22 +0200 | chaieb | added Theorem all_not_ex | file | diff | annotate |
| Thu, 14 Jun 2007 18:33:31 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
| Tue, 05 Jun 2007 19:23:09 +0200 | haftmann | tuned boostrap | file | diff | annotate |
| Tue, 05 Jun 2007 15:16:08 +0200 | haftmann | merged Code_Generator.thy into HOL.thy | file | diff | annotate |
| Thu, 31 May 2007 20:55:29 +0200 | wenzelm | moved IsaPlanner from Provers to Tools; | file | diff | annotate |
| Thu, 31 May 2007 18:16:51 +0200 | wenzelm | proper loading of ML files; | file | diff | annotate |
| Sat, 19 May 2007 19:08:42 +0200 | chaieb | added a set of NNF normalization lemmas and nnf_conv | file | diff | annotate |
| Thu, 17 May 2007 19:49:16 +0200 | haftmann | tuned | file | diff | annotate |
| Sun, 06 May 2007 21:49:24 +0200 | haftmann | dropped HOL.ML | file | diff | annotate |
| Fri, 20 Apr 2007 11:21:42 +0200 | haftmann | Isar definitions are now added explicitly to code theorem table | file | diff | annotate |
| Tue, 20 Mar 2007 15:52:38 +0100 | haftmann | added class "default" and expansion axioms for undefined | file | diff | annotate |
| Tue, 20 Mar 2007 08:27:15 +0100 | haftmann | explizit "type" superclass | file | diff | annotate |