Tue, 19 Dec 2006 17:35:33 +0100 aspinall Missing elements from doc_markup_elements
Tue, 19 Dec 2006 16:58:30 +0100 aspinall Remove obsolete prefixes from error and warning messages.
Mon, 18 Dec 2006 08:57:41 +0100 haftmann added isatool codegen
Mon, 18 Dec 2006 08:21:40 +0100 haftmann dropped CodegenPackage.const_of_idf
Mon, 18 Dec 2006 08:21:39 +0100 haftmann improvements in syntax handling
Mon, 18 Dec 2006 08:21:38 +0100 haftmann added Thyname.* and * constant expressions
Mon, 18 Dec 2006 08:21:37 +0100 haftmann introduces "__" naming policy
Mon, 18 Dec 2006 08:21:35 +0100 haftmann switched argument order in *.syntax lifters
Mon, 18 Dec 2006 08:21:34 +0100 haftmann added gen_reflection_tac
Mon, 18 Dec 2006 08:21:33 +0100 haftmann now testing executable content of nearly all HOL
Mon, 18 Dec 2006 08:21:32 +0100 haftmann dropped debug cmd
Mon, 18 Dec 2006 08:21:31 +0100 haftmann explicit nonfix declaration for ML "subset"
Mon, 18 Dec 2006 08:21:30 +0100 haftmann dropped two inline directives
Mon, 18 Dec 2006 08:21:29 +0100 haftmann introduced abstract view on number expressions in hologic.ML
Mon, 18 Dec 2006 08:21:28 +0100 haftmann whitespace fix
Mon, 18 Dec 2006 08:21:27 +0100 haftmann added code generation syntax for some char combinators
Mon, 18 Dec 2006 08:21:26 +0100 haftmann infix syntax for generated code for composition
Mon, 18 Dec 2006 08:21:25 +0100 haftmann new-style oracle setup
Mon, 18 Dec 2006 08:21:24 +0100 haftmann added functions tutorial
Sun, 17 Dec 2006 22:43:50 +0100 aspinall Add abstraction for objtypes and documents.
Sat, 16 Dec 2006 20:27:56 +0100 huffman removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy
Sat, 16 Dec 2006 20:23:45 +0100 huffman moved several theorems; rearranged theory dependencies
Sat, 16 Dec 2006 19:37:07 +0100 huffman hypreal_of_hypnat abbreviates more general of_hypnat
Fri, 15 Dec 2006 17:51:07 +0100 webertj tracing instead of warning
Fri, 15 Dec 2006 00:08:50 +0100 wenzelm updated;
Fri, 15 Dec 2006 00:08:16 +0100 wenzelm removed obsolete assert;
Fri, 15 Dec 2006 00:08:15 +0100 wenzelm renamed LocalTheory.assert to affirm;
Fri, 15 Dec 2006 00:08:14 +0100 wenzelm tuned -- accomodate Alice;
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
Thu, 14 Dec 2006 22:19:39 +0100 huffman remove Hyperreal/fuf.ML
Thu, 14 Dec 2006 22:18:08 +0100 huffman remove commented section
Thu, 14 Dec 2006 22:09:26 +0100 huffman remove ultra tactic and redundant FreeUltrafilterNat lemmas
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip