Wed, 22 Feb 2006 22:18:42 +0100 wenzelm removed obsolete meta_conjunction_tr';
Wed, 22 Feb 2006 22:18:41 +0100 wenzelm rew: handle conjunctionI/D1/D2;
Wed, 22 Feb 2006 22:18:39 +0100 wenzelm simplified Pure conjunction, based on actual const;
Wed, 22 Feb 2006 22:18:38 +0100 wenzelm removed rename_indexes_wrt;
Wed, 22 Feb 2006 22:18:36 +0100 wenzelm renamed class_axms to class_intros;
Wed, 22 Feb 2006 22:18:33 +0100 wenzelm tuned proofs;
Wed, 22 Feb 2006 22:18:32 +0100 wenzelm simplified Pure conjunction;
Wed, 22 Feb 2006 22:18:31 +0100 wenzelm not_equal: replaced syntax translation by abbreviation;
Wed, 22 Feb 2006 10:18:17 +0100 haftmann abandoned merge_alists' in favour of generic AList.merge
Tue, 21 Feb 2006 16:37:54 +0100 nipkow added Tools/nbe, fixes
Tue, 21 Feb 2006 16:37:33 +0100 nipkow added Tools/nbe
Tue, 21 Feb 2006 16:18:50 +0100 nipkow New normalization-by-evaluation package
Tue, 21 Feb 2006 15:06:50 +0100 wenzelm distinct (op =);
Mon, 20 Feb 2006 21:51:50 +0100 kleing fixed
Mon, 20 Feb 2006 16:23:38 +0100 paulson Inclusion of subset_refl in ATP calls
Mon, 20 Feb 2006 16:22:52 +0100 paulson Fix variable-naming bug (?) by removing a needless recursive call
Mon, 20 Feb 2006 11:38:06 +0100 haftmann slight code generator serialization improvements
Mon, 20 Feb 2006 11:37:18 +0100 haftmann moved intro_classes from AxClass to ClassPackage
Sun, 19 Feb 2006 22:40:18 +0100 kleing fixed document
Sun, 19 Feb 2006 22:12:30 +0100 kleing * denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
Sun, 19 Feb 2006 17:18:39 +0100 urbanc added a few lemmas to do with permutation-equivalence for the
Sun, 19 Feb 2006 13:21:32 +0100 kleing * added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
Sun, 19 Feb 2006 02:11:27 +0100 huffman use minimal imports
Sun, 19 Feb 2006 01:40:13 +0100 huffman use qualified name for return
Sat, 18 Feb 2006 18:08:23 +0100 wenzelm dest_def: tuned error msg;
Fri, 17 Feb 2006 20:03:21 +0100 wenzelm const constraints: provide TFrees instead of TVars,
Fri, 17 Feb 2006 20:03:19 +0100 wenzelm checkpoint/copy_node: reset body context;
Fri, 17 Feb 2006 20:03:17 +0100 wenzelm global_qeds: transfer body context;
Fri, 17 Feb 2006 20:03:14 +0100 wenzelm add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
Fri, 17 Feb 2006 20:03:10 +0100 wenzelm constrain: assert const declaration, optional type (i.e. may delete constraints);
Fri, 17 Feb 2006 17:00:33 +0100 wenzelm removed Import/lazy_scan.ML;
Fri, 17 Feb 2006 15:43:46 +0100 paulson hyperlinks in the PDF work now
Fri, 17 Feb 2006 15:03:26 +0100 obua replaced Symbol.explode by explode
Fri, 17 Feb 2006 08:42:41 +0100 haftmann updated mailing list archive link
Fri, 17 Feb 2006 03:30:50 +0100 obua use monomorphic sequences / scanners
Fri, 17 Feb 2006 01:46:38 +0100 huffman make maybe into a real type constructor; remove monad syntax
Thu, 16 Feb 2006 23:40:32 +0100 obua use VectorScannerSeq instead of ListScannerSeq in xml.ML
Thu, 16 Feb 2006 23:31:32 +0100 obua removed lazy_scan
Thu, 16 Feb 2006 23:30:47 +0100 obua improved scanning
Thu, 16 Feb 2006 21:15:38 +0100 wenzelm tuned;
Thu, 16 Feb 2006 21:12:03 +0100 wenzelm Abstract Natural Numbers with polymorphic recursion.
Thu, 16 Feb 2006 21:12:00 +0100 wenzelm new-style definitions/abbreviations;
Thu, 16 Feb 2006 21:11:58 +0100 wenzelm added ex/Abstract_NAT.thy;
Thu, 16 Feb 2006 19:39:02 +0100 wenzelm tuned;
Thu, 16 Feb 2006 19:10:47 +0100 wenzelm tuned;
Thu, 16 Feb 2006 18:59:39 +0100 haftmann removed silly stuff
Thu, 16 Feb 2006 18:39:48 +0100 wenzelm * Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
Thu, 16 Feb 2006 18:26:04 +0100 wenzelm added abbreviation(_i);
Thu, 16 Feb 2006 18:26:03 +0100 wenzelm added put_thms_internal: local_naming, no fact index;
Thu, 16 Feb 2006 18:26:02 +0100 wenzelm added put_thms_internal;
Thu, 16 Feb 2006 18:26:01 +0100 wenzelm added abbrev element;
Thu, 16 Feb 2006 18:26:00 +0100 wenzelm added 'abbreviation';
Thu, 16 Feb 2006 18:25:58 +0100 wenzelm added premsN;
Thu, 16 Feb 2006 18:25:58 +0100 wenzelm Proof.put_thms_internal;
Thu, 16 Feb 2006 18:25:56 +0100 wenzelm removed pointless replace;
Thu, 16 Feb 2006 18:25:55 +0100 wenzelm tuned;
Thu, 16 Feb 2006 18:25:55 +0100 wenzelm dest_def: actually return beta-eta contracted equation;
Thu, 16 Feb 2006 18:25:54 +0100 wenzelm derived specifications: definition, abbreviation, axiomatization;
Thu, 16 Feb 2006 18:25:52 +0100 wenzelm updated;
Thu, 16 Feb 2006 14:59:57 +0100 obua cache improvements
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip