2005-09-13 ago wenzelm tuned;
2005-09-13 ago wenzelm more self-contained proof elements (material from isar_thy.ML);
2005-09-13 ago wenzelm added cases, rule_contextN;
2005-09-13 ago wenzelm load locale.ML late (after proof.ML);
2005-09-13 ago wenzelm added maps, map_list, lift, lifts;
2005-09-13 ago wenzelm added stack.ML;
2005-09-13 ago wenzelm added simple_fact;
2005-09-13 ago wenzelm Seq.maps;
2005-09-13 ago wenzelm added hide_names(_i) (from isar_thy.ML);
2005-09-13 ago wenzelm added generic_setup, add_oracle (from isar_thy.ML);
2005-09-13 ago wenzelm added exception EXCEPTION of exn * string;
2005-09-13 ago wenzelm replaced DATA_FAIL by EXCEPTION;
2005-09-13 ago wenzelm tuned Isar interfaces;
2005-09-13 ago wenzelm added General/stack.ML, Isar/proof_display.ML;
2005-09-13 ago wenzelm the_list (cf. Pure/library.ML);
2005-09-13 ago wenzelm tuned IsarThy.theorem_i;
2005-09-13 ago obua fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-12 ago huffman list of constants and theorems whose names have been changed or merged
2005-09-12 ago huffman add header
2005-09-12 ago huffman added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12 ago huffman updated to work with latest HOL-Complex
2005-09-12 ago huffman add file Hyperreal/transfer.ML
2005-09-12 ago huffman new implementation of transfer principle
2005-09-12 ago obua removed clutter
2005-09-12 ago nipkow name conflict with global itrev resolved
2005-09-12 ago nipkow dealt with name clash with List.itrev
2005-09-12 ago haftmann introduced new-style AList operations
2005-09-12 ago obua introduced internal function hthm2thm
2005-09-12 ago obua 1) Added target HOL-Complex-Generate-HOLLight
2005-09-12 ago obua Added HOLLight support to importer.
2005-09-12 ago wenzelm added interact flag to control mode of excursions;
2005-09-11 ago wenzelm excursion: interactive if debug;
2005-09-09 ago huffman updated to work with new HOL-Complex version
2005-09-09 ago huffman starfun, starset, and other functions on NS types are now polymorphic;
2005-09-09 ago paulson Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-09 ago ballarin fixed printing of locales
2005-09-08 ago paulson consolidation of duplicate code in Isabelle-ATP linkup
2005-09-08 ago haftmann introduces some modern-style AList operations
2005-09-08 ago haftmann added the_list, the_default
2005-09-08 ago paulson yet more tidying of Isabelle-ATP link
2005-09-07 ago wenzelm converted to Isar theory format;
2005-09-07 ago wenzelm converted to Isar theory format;
2005-09-07 ago wenzelm converted to Isar theory format;
2005-09-07 ago wenzelm removed TLA/Inc/Pcount.thy;
2005-09-07 ago paulson elimination of watcher.sig
2005-09-07 ago paulson Progress on eprover linkup, also massive tidying
2005-09-07 ago paulson axioms now included in tptp files, no /bin/cat and various tidying
2005-09-07 ago paulson consolidation of watcher.ML and watcher.sig
2005-09-07 ago huffman generalized types more
2005-09-07 ago huffman generalized types
2005-09-07 ago huffman added theorem hypreal_inverse2
2005-09-07 ago huffman replace type hcomplex with complex star
2005-09-07 ago huffman replace type hypnat with nat star
2005-09-06 ago huffman replace type hypreal with real star
2005-09-06 ago huffman add Hyperreal dependencies
2005-09-06 ago huffman class instances for nonstandard types
2005-09-06 ago huffman transfer principle tactic
2005-09-06 ago huffman generic nonstandard type constructor
2005-09-06 ago wenzelm converted to Isar theory format;
2005-09-06 ago huffman fix proof