2005-09-14 schirmer 2005-09-14 removed syntax fun_map_comp; introduced map_comp;
2005-09-14 chaieb 2005-09-14 Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
2005-09-14 wenzelm 2005-09-14 Method comm_ring for proving equalities in commutative rings.
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
2005-09-14 wenzelm 2005-09-14 fixed some ML names;
2005-09-14 wenzelm 2005-09-14 imports Commutative_Ring;
2005-09-14 wenzelm 2005-09-14 HOL: method comm_ring; Proof General: Unicode (UTF-8) support;
2005-09-14 wenzelm 2005-09-14 tuned;
2005-09-14 wenzelm 2005-09-14 no longer prefer xemacs, which fails more often than GNU emacs;
2005-09-14 wenzelm 2005-09-14 Bernhard Haeupler: comm_ring;
2005-09-14 chaieb 2005-09-14 tactic and the rest eliminated, just the theory....
2005-09-14 chaieb 2005-09-14 use was wrong...
2005-09-14 obua 2005-09-14 Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
2005-09-14 chaieb 2005-09-14 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy comm_ring : a reflected Method for proving equalities in a commutative ring
2005-09-14 haftmann 2005-09-14 introduced AList.lookup
2005-09-14 paulson 2005-09-14 correct E brackets
2005-09-14 paulson 2005-09-14 nice names for more infix operators
2005-09-14 haftmann 2005-09-14 introduces AList.lookup
2005-09-14 huffman 2005-09-14 removed duplicated lemmas; convert more proofs to transfer principle
2005-09-13 huffman 2005-09-13 add theorem chain_const
2005-09-13 wenzelm 2005-09-13 tuned;
2005-09-13 wenzelm 2005-09-13 global quick_and_dirty;
2005-09-13 wenzelm 2005-09-13 Printing of Isar proof elements etc.
2005-09-13 wenzelm 2005-09-13 Non-empty stacks.
2005-09-13 wenzelm 2005-09-13 IsarThy.begin_theory;
2005-09-13 wenzelm 2005-09-13 export ml_exts;
2005-09-13 wenzelm 2005-09-13 begin_theory: tuned interface, check uses;
2005-09-13 wenzelm 2005-09-13 replaced TRANSLATION_FAIL by EXCEPTION;
2005-09-13 wenzelm 2005-09-13 added three_buffersN, print3; tuned theory_to_proof: plain Proof.state instead of history; added EXCEPTION; removed DATA_FAIL, TRANSLATION_FAIL;
2005-09-13 wenzelm 2005-09-13 load before proof.ML; moved proof elements to proof.ML;
2005-09-13 wenzelm 2005-09-13 added simple; eliminated obsolete Sign.sg;
2005-09-13 wenzelm 2005-09-13 added add_view, export_view (supercedes adhoc view arguments); unified put_thms/reset_thms;
2005-09-13 wenzelm 2005-09-13 major cleanup of interfaces and implementation; generic goal commands: local/global_goal with after_qed; independent of locale.ML; more self-contained proof elements (material from isar_thy.ML); refer to ProofDisplay (cf. proof_display.ML); unified print_results (always normal); added get_thmss;
2005-09-13 wenzelm 2005-09-13 added name_facts;
2005-09-13 wenzelm 2005-09-13 tuned Isar proof elements;
2005-09-13 wenzelm 2005-09-13 added cheating, sorry_text (from skip_proofs.ML); added method_setup (from isar_thy.ML);
2005-09-13 wenzelm 2005-09-13 load late, after proof.ML; added goal commands: theorem, interpretation etc.; tuned some warnings -- single line only;
2005-09-13 wenzelm 2005-09-13 moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.); begin_theory: tuned interface, check uses in thy_info.ML;
2005-09-13 wenzelm 2005-09-13 cleanup parsers and interfaces;
2005-09-13 wenzelm 2005-09-13 Proof.get_thmss;
2005-09-13 wenzelm 2005-09-13 tuned;
2005-09-13 wenzelm 2005-09-13 more self-contained proof elements (material from isar_thy.ML); tuned;
2005-09-13 wenzelm 2005-09-13 added cases, rule_contextN; eliminated obsolete Sign.sg;
2005-09-13 wenzelm 2005-09-13 load locale.ML late (after proof.ML); tuned module arrangement;
2005-09-13 wenzelm 2005-09-13 added maps, map_list, lift, lifts;
2005-09-13 wenzelm 2005-09-13 added stack.ML;
2005-09-13 wenzelm 2005-09-13 added simple_fact; generalized no_attributes;
2005-09-13 wenzelm 2005-09-13 Seq.maps;
2005-09-13 wenzelm 2005-09-13 added hide_names(_i) (from isar_thy.ML);
2005-09-13 wenzelm 2005-09-13 added generic_setup, add_oracle (from isar_thy.ML);
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