2005-09-13 wenzelm 2005-09-13 added exception EXCEPTION of exn * string;
2005-09-13 wenzelm 2005-09-13 replaced DATA_FAIL by EXCEPTION;
2005-09-13 wenzelm 2005-09-13 tuned Isar interfaces; tuned IsarThy.theorem_i;
2005-09-13 wenzelm 2005-09-13 added General/stack.ML, Isar/proof_display.ML;
2005-09-13 wenzelm 2005-09-13 the_list (cf. Pure/library.ML);
2005-09-13 wenzelm 2005-09-13 tuned IsarThy.theorem_i;
2005-09-13 obua 2005-09-13 fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-12 huffman 2005-09-12 list of constants and theorems whose names have been changed or merged
2005-09-12 huffman 2005-09-12 add header
2005-09-12 huffman 2005-09-12 added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12 huffman 2005-09-12 updated to work with latest HOL-Complex
2005-09-12 huffman 2005-09-12 add file Hyperreal/transfer.ML
2005-09-12 huffman 2005-09-12 new implementation of transfer principle
2005-09-12 obua 2005-09-12 removed clutter
2005-09-12 nipkow 2005-09-12 name conflict with global itrev resolved
2005-09-12 nipkow 2005-09-12 dealt with name clash with List.itrev
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-09-12 obua 2005-09-12 introduced internal function hthm2thm
2005-09-12 obua 2005-09-12 1) Added target HOL-Complex-Generate-HOLLight 2) Make heap image for HOL-Complex-Matrix
2005-09-12 obua 2005-09-12 Added HOLLight support to importer.
2005-09-12 wenzelm 2005-09-12 added interact flag to control mode of excursions;
2005-09-11 wenzelm 2005-09-11 excursion: interactive if debug;
2005-09-09 huffman 2005-09-09 updated to work with new HOL-Complex version
2005-09-09 huffman 2005-09-09 starfun, starset, and other functions on NS types are now polymorphic; many similar theorems have been generalized and merged; (star_n X) replaces (Abs_star(starrel `` {X})); many proofs have been simplified with the transfer tactic.
2005-09-09 paulson 2005-09-09 Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-09 ballarin 2005-09-09 fixed printing of locales
2005-09-08 paulson 2005-09-08 consolidation of duplicate code in Isabelle-ATP linkup
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-08 haftmann 2005-09-08 added the_list, the_default
2005-09-08 paulson 2005-09-08 yet more tidying of Isabelle-ATP link
2005-09-07 wenzelm 2005-09-07 converted to Isar theory format;
2005-09-07 wenzelm 2005-09-07 converted to Isar theory format;
2005-09-07 wenzelm 2005-09-07 converted to Isar theory format;
2005-09-07 wenzelm 2005-09-07 removed TLA/Inc/Pcount.thy;
2005-09-07 paulson 2005-09-07 elimination of watcher.sig
2005-09-07 paulson 2005-09-07 Progress on eprover linkup, also massive tidying
2005-09-07 paulson 2005-09-07 axioms now included in tptp files, no /bin/cat and various tidying
2005-09-07 paulson 2005-09-07 consolidation of watcher.ML and watcher.sig
2005-09-07 huffman 2005-09-07 generalized types more
2005-09-07 huffman 2005-09-07 generalized types
2005-09-07 huffman 2005-09-07 added theorem hypreal_inverse2
2005-09-07 huffman 2005-09-07 replace type hcomplex with complex star
2005-09-07 huffman 2005-09-07 replace type hypnat with nat star
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
2005-09-06 huffman 2005-09-06 add Hyperreal dependencies
2005-09-06 huffman 2005-09-06 class instances for nonstandard types
2005-09-06 huffman 2005-09-06 transfer principle tactic
2005-09-06 huffman 2005-09-06 generic nonstandard type constructor
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-09-06 huffman 2005-09-06 fix proof
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-09-06 huffman 2005-09-06 reimplement Filter.thy with locales
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-09-06 wenzelm 2005-09-06 removed some ML files in Modelcheck/;
2005-09-06 wenzelm 2005-09-06 updated;
2005-09-06 wenzelm 2005-09-06 axclass: no longer bind "cI";
2005-09-06 wenzelm 2005-09-06 deprecated old-style infix declarations, which mix name and syntax;
2005-09-06 wenzelm 2005-09-06 tuned msg;
2005-09-06 wenzelm 2005-09-06 AList.defined;