Thu, 14 Dec 2006 22:08:35 +0100 huffman declare insert_iff [simp]
Thu, 14 Dec 2006 21:46:59 +0100 wenzelm activated improved use_ml, which captures output and reports source positions;
Thu, 14 Dec 2006 21:46:58 +0100 wenzelm tuned;
Thu, 14 Dec 2006 21:33:47 +0100 huffman prove hyperpow_realpow using transfer
Thu, 14 Dec 2006 21:03:39 +0100 huffman remove usage of ultra tactic
Thu, 14 Dec 2006 19:29:48 +0100 huffman add lemmas singleton and insert_iff
Thu, 14 Dec 2006 19:15:16 +0100 huffman generalized type of hyperpow; removed hcpow
Thu, 14 Dec 2006 18:10:38 +0100 huffman redefine hSuc as *f* Suc, and move to HyperNat.thy
Thu, 14 Dec 2006 16:08:09 +0100 wenzelm proper use of IntInf instead of InfInf;
Thu, 14 Dec 2006 15:31:22 +0100 wenzelm defs/notes: more robust transitivity reasoning;
Thu, 14 Dec 2006 15:31:21 +0100 wenzelm added trans_terms/props;
Thu, 14 Dec 2006 15:31:20 +0100 wenzelm locale: print context for begin;
Thu, 14 Dec 2006 01:19:27 +0100 huffman remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq
Wed, 13 Dec 2006 23:15:39 +0100 huffman remove uses of star_n and FreeUltrafilterNat
Wed, 13 Dec 2006 21:46:34 +0100 huffman remove use of FreeUltrafilterNat
Wed, 13 Dec 2006 21:25:56 +0100 huffman added lemmas about hRe, hIm, HComplex; removed all uses of star_n
Wed, 13 Dec 2006 20:38:24 +0100 haftmann fixed type
Wed, 13 Dec 2006 20:38:23 +0100 haftmann added stub for OCaml serializer
Wed, 13 Dec 2006 20:38:20 +0100 haftmann cleanup
Wed, 13 Dec 2006 20:38:19 +0100 haftmann whitespace correction
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip