Wed, 13 Dec 2006 20:38:18 +0100 haftmann clarifed comment
Wed, 13 Dec 2006 20:38:17 +0100 haftmann dropped FIXME comment
Wed, 13 Dec 2006 20:38:16 +0100 haftmann clarified character setup
Wed, 13 Dec 2006 19:39:48 +0100 huffman remove references to star_n
Wed, 13 Dec 2006 19:05:45 +0100 huffman SComplex abbreviates Standard
Wed, 13 Dec 2006 16:33:11 +0100 wenzelm simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
Wed, 13 Dec 2006 16:32:20 +0100 wenzelm removed legacy ML bindings;
Wed, 13 Dec 2006 16:26:45 +0100 wenzelm updated;
Wed, 13 Dec 2006 15:47:37 +0100 wenzelm tuned signature;
Wed, 13 Dec 2006 15:47:36 +0100 wenzelm internal_abbrev: observe print mode;
Wed, 13 Dec 2006 15:47:34 +0100 wenzelm target_abbrev: internal mode for abbrevs;
Wed, 13 Dec 2006 15:47:33 +0100 wenzelm edge: actually apply operation!
Wed, 13 Dec 2006 15:47:31 +0100 wenzelm tuned;
Wed, 13 Dec 2006 15:45:33 +0100 haftmann authentic syntax for number_of
Wed, 13 Dec 2006 15:45:31 +0100 haftmann introduced mk/dest_numeral/number for mk/dest_binum etc.
Wed, 13 Dec 2006 15:45:30 +0100 haftmann fixed syntax for bounded quantification
Wed, 13 Dec 2006 15:45:29 +0100 haftmann dropped superfluous header
Wed, 13 Dec 2006 14:56:50 +0100 krauss clarified error message
Wed, 13 Dec 2006 14:54:07 +0100 krauss nat type now has a size functin => no longer needed as special case
Wed, 13 Dec 2006 14:52:50 +0100 krauss simplified
Wed, 13 Dec 2006 14:52:30 +0100 wenzelm local_abbrev: proper fix/declare of local entities;
Wed, 13 Dec 2006 12:42:26 +0100 paulson Deleted the unused type argument of UVar
Wed, 13 Dec 2006 12:10:54 +0100 wenzelm tuned comments;
Wed, 13 Dec 2006 12:07:43 +0100 krauss added IsarAdvanced/Functions
Wed, 13 Dec 2006 00:07:13 +0100 huffman generalized some lemmas; removed redundant lemmas; cleaned up some proofs
Wed, 13 Dec 2006 00:02:53 +0100 huffman remove uses of scaleR infix syntax; add lemma Reals_number_of
Tue, 12 Dec 2006 21:25:14 +0100 wenzelm tuned;
Tue, 12 Dec 2006 21:25:13 +0100 wenzelm add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
Tue, 12 Dec 2006 20:50:23 +0100 wenzelm updated;
Tue, 12 Dec 2006 20:49:32 +0100 wenzelm simplified unlocalize_mixfix;
Tue, 12 Dec 2006 20:49:31 +0100 wenzelm removed is_class -- handled internally;
Tue, 12 Dec 2006 20:49:30 +0100 wenzelm notation: Term.equiv_types;
Tue, 12 Dec 2006 20:49:29 +0100 wenzelm abbrev: tuned signature;
Tue, 12 Dec 2006 20:49:28 +0100 wenzelm tuned expand_term;
Tue, 12 Dec 2006 20:49:27 +0100 wenzelm classified show/thus as prf_asm_goal, which is usually hilited in PG;
Tue, 12 Dec 2006 20:49:26 +0100 wenzelm tuned expand_binds;
Tue, 12 Dec 2006 20:49:25 +0100 wenzelm tuned error messages;
Tue, 12 Dec 2006 20:49:24 +0100 wenzelm added equiv_types;
Tue, 12 Dec 2006 20:49:23 +0100 wenzelm add_abbrev: tuned signature;
Tue, 12 Dec 2006 20:49:22 +0100 wenzelm added expand_term_frees;
Tue, 12 Dec 2006 20:49:21 +0100 wenzelm abbreviate: tuned signature;
Tue, 12 Dec 2006 20:49:19 +0100 wenzelm LocalTheory.abbrev;
Tue, 12 Dec 2006 17:29:26 +0100 huffman removed redundant constants and lemmas
Tue, 12 Dec 2006 17:15:42 +0100 huffman additions to HOL-Complex
Tue, 12 Dec 2006 16:20:57 +0100 paulson Removal of the "keep_types" flag: we always keep types!
Tue, 12 Dec 2006 12:03:46 +0100 wenzelm make SML/NJ happy;
Tue, 12 Dec 2006 11:57:30 +0100 wenzelm made SML/NJ happy;
Tue, 12 Dec 2006 07:46:40 +0100 huffman consistent naming for FreeUltrafilterNat lemmas; cleaned up
Tue, 12 Dec 2006 07:13:06 +0100 huffman cleaned up; generalized some proofs
Tue, 12 Dec 2006 07:11:58 +0100 huffman fix assumptions on NSDERIV_quotient
Tue, 12 Dec 2006 04:37:25 +0100 huffman changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
Tue, 12 Dec 2006 04:32:50 +0100 huffman generalize some theorems
Tue, 12 Dec 2006 04:31:34 +0100 huffman add type annotation
Tue, 12 Dec 2006 00:25:09 +0100 wenzelm read_xnum: return leading_zeros, radix;
Tue, 12 Dec 2006 00:25:05 +0100 wenzelm authentic syntax for Pls/Min/Bit;
Tue, 12 Dec 2006 00:25:03 +0100 wenzelm authentic syntax for Pls/Min/Bit;
Tue, 12 Dec 2006 00:25:02 +0100 wenzelm binary numerals: restricted to actual abstract syntax;
Tue, 12 Dec 2006 00:03:42 +0100 huffman Hyperreal/FrechetDeriv.thy
Tue, 12 Dec 2006 00:02:54 +0100 huffman theory of Frechet derivatives
Mon, 11 Dec 2006 21:41:05 +0100 wenzelm specials: include single quote;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip