2005-09-06 webertj 2005-09-06 unnecessary parentheses removed
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-09-06 haftmann 2005-09-06 eliminated 1 call to polyEq
2005-09-05 wenzelm 2005-09-05 tuned;
2005-09-05 wenzelm 2005-09-05 updated;
2005-09-05 wenzelm 2005-09-05 obsolete;
2005-09-05 wenzelm 2005-09-05 added assert, command;
2005-09-05 wenzelm 2005-09-05 tuned check_text;
2005-09-05 wenzelm 2005-09-05 chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05 wenzelm 2005-09-05 markup commands: optional locale specification;
2005-09-05 wenzelm 2005-09-05 add_chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-09-05 wenzelm 2005-09-05 tuned;
2005-09-05 wenzelm 2005-09-05 Markup commands 'chapter' .. 'text' support optional locale specification;
2005-09-05 wenzelm 2005-09-05 removed duplicate theorems;
2005-09-05 haftmann 2005-09-05 introduced binding priority 1 for linear combinators etc.
2005-09-03 wenzelm 2005-09-03 converted to Isar theory format;
2005-09-03 wenzelm 2005-09-03 tuned method;
2005-09-03 wenzelm 2005-09-03 tuned;
2005-09-03 wenzelm 2005-09-03 obsolete;
2005-09-03 wenzelm 2005-09-03 converted to Isar theory format;
2005-09-03 wenzelm 2005-09-03 obsolete (see Cube.thy);
2005-09-03 wenzelm 2005-09-03 tuned msg;
2005-09-03 wenzelm 2005-09-03 uses ("LCF_lemmas.ML");
2005-09-03 wenzelm 2005-09-03 converted to Isar theory format;
2005-09-03 wenzelm 2005-09-03 tuned;
2005-09-03 wenzelm 2005-09-03 removed fix.thy, pair.thy, simpdata.ML; renamed LCF.ML to LCF_lemmas.ML;
2005-09-03 wenzelm 2005-09-03 converted to Isar theory format;
2005-09-03 wenzelm 2005-09-03 converted to Isar theory format;
2005-09-03 wenzelm 2005-09-03 setmp print_mode []; more robust outer syntax; tuned;
2005-09-03 wenzelm 2005-09-03 tuned;
2005-09-03 wenzelm 2005-09-03 simplified oracle;
2005-09-03 wenzelm 2005-09-03 use Check.ML;
2005-09-03 wenzelm 2005-09-03 fixed ML errors;
2005-09-03 wenzelm 2005-09-03 removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
2005-09-03 wenzelm 2005-09-03 deprecated non-Isar theory file format;
2005-09-02 quigley 2005-09-02 Added ECommunication.ML
2005-09-02 quigley 2005-09-02 Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and recon_transfer_proof.ML to deal with the E theorem prover.
2005-09-02 paulson 2005-09-02 further tidying up of Isabelle-ATP link
2005-09-02 wenzelm 2005-09-02 converted specifications to Isar theories;
2005-09-02 haftmann 2005-09-02 some 'assoc' etc. refactoring
2005-09-02 paulson 2005-09-02 tidying up the Isabelle/ATP interface
2005-09-02 paulson 2005-09-02 fixed arities and restored changes that had gone missing
2005-09-02 paulson 2005-09-02 deleted obsolete VampireCommunication.ML
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-09-01 wenzelm 2005-09-01 refrain from sorting output;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; removed obsolete current_sign; tuned;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
2005-09-01 wenzelm 2005-09-01 added curried_lookup/update operations -- in preparation of currying plain lookup/update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-09-01 wenzelm 2005-09-01 updated;
2005-09-01 wenzelm 2005-09-01 renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;
2005-09-01 wenzelm 2005-09-01 removed obsolete 'symbols' mode;
2005-09-01 wenzelm 2005-09-01 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z; tuned;
2005-09-01 paulson 2005-09-01 improved formatting
2005-09-01 wenzelm 2005-09-01 isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;
2005-09-01 wenzelm 2005-09-01 updated;