2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 wenzelm 2005-09-20 tuned simprocs;
2005-09-20 wenzelm 2005-09-20 removed Commutative_Ring hacks;
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-09-20 wenzelm 2005-09-20 removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 wenzelm 2005-09-20 Chinese Unicode example;
2005-09-20 wenzelm 2005-09-20 tuned proofs;
2005-09-20 chaieb 2005-09-20 The simpset of the actual theory is take, in order to handle rings defined after the method
2005-09-20 paulson 2005-09-20 further tidying; killing of old Watcher loops
2005-09-20 nipkow 2005-09-20 added a number of lemmas
2005-09-20 paulson 2005-09-20 uniform handling of interrupts
2005-09-20 chaieb 2005-09-20 algebra method added.
2005-09-20 haftmann 2005-09-20 improved eq_fst and eq_snd, removed some deprecated stuff
2005-09-20 haftmann 2005-09-20 added make and find
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-20 haftmann 2005-09-20 infix operator precedence
2005-09-20 webertj 2005-09-20 using curried Inttab.update_new function now
2005-09-19 webertj 2005-09-19 SAT solver interface modified to support proofs of unsatisfiability
2005-09-19 wenzelm 2005-09-19 shrink: compress terms and types; prefer member/insert over polymorphic mem/ins;
2005-09-19 wenzelm 2005-09-19 added String.isSuffix;
2005-09-19 obua 2005-09-19 maybe the last bug fix (sigh)?
2005-09-19 obua 2005-09-19 Removed superfluous HOL/Matrix/cplex/ROOT.ML.
2005-09-19 paulson 2005-09-19 further simplification of the Isabelle-ATP linkup
2005-09-19 haftmann 2005-09-19 added make function
2005-09-19 haftmann 2005-09-19 removed some deprecated assocation list functions
2005-09-19 haftmann 2005-09-19 introduced AList module
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-19 kleing 2005-09-19 update usage message
2005-09-19 wenzelm 2005-09-19 obsolete;
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;