2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
2005-09-17 wenzelm 2005-09-17 converted to Isar theory format;
2005-09-17 wenzelm 2005-09-17 tuned;
2005-09-17 wenzelm 2005-09-17 converted to Isar theory format;
2005-09-17 wenzelm 2005-09-17 moved quick_and_dirty to Pure/ROOT.ML;
2005-09-17 wenzelm 2005-09-17 pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17 wenzelm 2005-09-17 added quick_and_dirty (from Isar/skip_proofs.ML);
2005-09-17 wenzelm 2005-09-17 manually generated from Isabelle/HOLCF/IOA/Complex/Import;
2005-09-17 wenzelm 2005-09-17 tuned document;
2005-09-17 wenzelm 2005-09-17 tuned;
2005-09-17 wenzelm 2005-09-17 added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
2005-09-17 wenzelm 2005-09-17 tuned comments;
2005-09-17 wenzelm 2005-09-17 pretty_thm_aux: aconv hyps;
2005-09-17 wenzelm 2005-09-17 removed obsolete BasisLibrary; proof_general.ML: setmp proofs 1 to capture sane default preferences;
2005-09-17 wenzelm 2005-09-17 Hebrew: HTML.with_charset;
2005-09-17 wenzelm 2005-09-17 removed obsolete BasisLibrary;
2005-09-17 wenzelm 2005-09-17 added quickcheck_params (from Main.thy);
2005-09-17 wenzelm 2005-09-17 removed spurious PolyML.exception_trace;
2005-09-17 wenzelm 2005-09-17 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
2005-09-17 wenzelm 2005-09-17 minor cleanup, moved stuff in its proper place;
2005-09-17 wenzelm 2005-09-17 generate: added HOL-Complex-Generate-HOLLight;
2005-09-17 wenzelm 2005-09-17 added code generator setup (from Main.thy);
2005-09-17 wenzelm 2005-09-17 lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
2005-09-17 wenzelm 2005-09-17 HTML.with_charset;
2005-09-17 wenzelm 2005-09-17 converted to Isar theory format;
2005-09-17 wenzelm 2005-09-17 tuned document;
2005-09-17 wenzelm 2005-09-17 obsolete;
2005-09-17 wenzelm 2005-09-17 plain test session, includes example;
2005-09-17 wenzelm 2005-09-17 theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-17 wenzelm 2005-09-17 added auto_fix (from proof.ML); added assms_of; removed assumptions_of; pretty_thm: show out-of-context hyps; warn_extra_tfrees: works again, tuned;
2005-09-17 wenzelm 2005-09-17 export put_facts; moved auto_fix to proof_context.ML; generic_goal: solve 0 subgoals initially; global_goal/theorem: only store results if SOME target, which may be empty;
2005-09-17 wenzelm 2005-09-17 interpretation: use goal commands without target -- no storing of results;
2005-09-17 wenzelm 2005-09-17 theorem(_i): empty target; forget_proof: removed tmp hack;
2005-09-17 wenzelm 2005-09-17 pretty_thm_aux: observe asms context;
2005-09-17 wenzelm 2005-09-17 tuned;
2005-09-17 wenzelm 2005-09-17 Cube: converted to Isar, use locales;
2005-09-17 obua 2005-09-17 1) mapped .. and == constants 2) improved protect_varname
2005-09-17 huffman 2005-09-17 use interpretation command
2005-09-16 huffman 2005-09-16 add HOLCF entries for pcpodef, cont_proc, fixrec; add HOL-Complex entry for transfer tactic; clean up lists of theories in HOL-Complex entries
2005-09-16 wenzelm 2005-09-16 converted to Isar theory format;
2005-09-16 obua 2005-09-16 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
2005-09-16 huffman 2005-09-16 add header
2005-09-16 ballarin 2005-09-16 tuned
2005-09-16 ballarin 2005-09-16 interpretation uses primitive goal interface
2005-09-16 ballarin 2005-09-16 tuned
2005-09-16 paulson 2005-09-16 PARTIAL conversion to Vampire8
2005-09-16 paulson 2005-09-16 catching exception Io
2005-09-16 huffman 2005-09-16 rearranged
2005-09-16 huffman 2005-09-16 use mem operator
2005-09-16 huffman 2005-09-16 fix names in hypreal_arith.ML
2005-09-15 huffman 2005-09-15 merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
2005-09-15 huffman 2005-09-15 merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-15 huffman 2005-09-15 add header
2005-09-15 chaieb 2005-09-15 The SMLNJ Problem fixed...
2005-09-15 chaieb 2005-09-15 getting it work for SMLNJ
2005-09-15 wenzelm 2005-09-15 * Improved efficiency of the Simplifier etc.;
2005-09-15 wenzelm 2005-09-15 incorporated into NEWS;
2005-09-15 wenzelm 2005-09-15 incorporated HOL/Hyperreal/CHANGES;
2005-09-15 paulson 2005-09-15 massive tidy-up and simplification