| Wed, 02 Jan 2008 15:14:02 +0100 | haftmann | splitted class uminus from class minus | file | diff | annotate |
| Fri, 30 Nov 2007 20:13:03 +0100 | haftmann | adjustions to due to instance target | file | diff | annotate |
| Thu, 29 Nov 2007 17:08:26 +0100 | haftmann | instance command as rudimentary class target | file | diff | annotate |
| Fri, 23 Nov 2007 21:09:33 +0100 | haftmann | interpretation of typedecls: instantiation to class type | file | diff | annotate |
| Fri, 09 Nov 2007 13:41:27 +0100 | krauss | avoid name clashes when generating code for union, inter | file | diff | annotate |
| Mon, 05 Nov 2007 18:18:39 +0100 | nipkow | added lemmas | file | diff | annotate |
| Wed, 26 Sep 2007 20:27:58 +0200 | haftmann | convenient obtain rule for sets | file | diff | annotate |
| Thu, 20 Sep 2007 16:37:30 +0200 | haftmann | clarified code lemmas | file | diff | annotate |
| Fri, 24 Aug 2007 14:14:16 +0200 | haftmann | made sets executable | file | diff | annotate |
| Sun, 19 Aug 2007 21:21:37 +0200 | nipkow | Made UN_Un simp | file | diff | annotate |
| Fri, 17 Aug 2007 13:58:57 +0200 | haftmann | dropped junk | file | diff | annotate |
| Wed, 15 Aug 2007 12:52:56 +0200 | paulson | ATP blacklisting is now in theory data, attribute noatp | file | diff | annotate |
| Wed, 15 Aug 2007 08:57:39 +0200 | haftmann | updated code generator setup | file | diff | annotate |
| Fri, 20 Jul 2007 14:27:56 +0200 | haftmann | simplified HOL bootstrap | file | diff | annotate |
| Thu, 19 Jul 2007 21:47:44 +0200 | haftmann | code lemma for contents | file | diff | annotate |
| Sun, 06 May 2007 21:50:17 +0200 | haftmann | changed code generator invocation syntax | 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 08:27:23 +0100 | haftmann | fixed typo | file | diff | annotate |
| Fri, 16 Mar 2007 21:32:11 +0100 | haftmann | added instance of sets as distributive lattices | file | diff | annotate |
| Mon, 12 Mar 2007 19:23:49 +0100 | wenzelm | syntax: proper body priorty for derived binders; | file | diff | annotate |
| Wed, 28 Feb 2007 22:05:43 +0100 | wenzelm | tuned ML setup; | file | diff | annotate |
| Wed, 24 Jan 2007 17:10:50 +0100 | paulson | some new lemmas | file | diff | annotate |
| Sat, 20 Jan 2007 14:09:27 +0100 | wenzelm | tuned ML setup; | file | diff | annotate |
| Wed, 13 Dec 2006 20:38:17 +0100 | haftmann | dropped FIXME comment | file | diff | annotate |
| Wed, 13 Dec 2006 15:45:30 +0100 | haftmann | fixed syntax for bounded quantification | file | diff | annotate |
| Wed, 06 Dec 2006 01:12:36 +0100 | wenzelm | removed legacy ML bindings; | file | diff | annotate |
| Mon, 27 Nov 2006 13:42:42 +0100 | haftmann | restructured some proofs | file | diff | annotate |
| Sun, 26 Nov 2006 18:07:16 +0100 | wenzelm | updated (binder) syntax/notation; | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Wed, 15 Nov 2006 17:05:43 +0100 | haftmann | moved transitivity rules to Orderings.thy | file | diff | annotate |