fixed some ML names;

imports Commutative_Ring;

HOL: method comm_ring; Proof General: Unicode (UTF-8) support;

tuned;

no longer prefer xemacs, which fails more often than GNU emacs;

Bernhard Haeupler: comm_ring;

tactic and the rest eliminated, just the theory....

use was wrong...

Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.

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

introduced AList.lookup

correct E brackets

nice names for more infix operators

introduces AList.lookup

removed duplicated lemmas; convert more proofs to transfer principle

add theorem chain_const

tuned;

global quick_and_dirty;

Printing of Isar proof elements etc.

Non-empty stacks.

IsarThy.begin_theory;

export ml_exts;

begin_theory: tuned interface, check uses;

replaced TRANSLATION_FAIL by EXCEPTION;

added three_buffersN, print3; tuned theory_to_proof: plain Proof.state instead of history; added EXCEPTION; removed DATA_FAIL, TRANSLATION_FAIL;

load before proof.ML; moved proof elements to proof.ML;

added simple; eliminated obsolete Sign.sg;

added add_view, export_view (supercedes adhoc view arguments); unified put_thms/reset_thms;

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;

added name_facts;

tuned Isar proof elements;

added cheating, sorry_text (from skip_proofs.ML); added method_setup (from isar_thy.ML);

load late, after proof.ML; added goal commands: theorem, interpretation etc.; tuned some warnings -- single line only;

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;

cleanup parsers and interfaces;

Proof.get_thmss;

tuned;

more self-contained proof elements (material from isar_thy.ML); tuned;

added cases, rule_contextN; eliminated obsolete Sign.sg;

load locale.ML late (after proof.ML); tuned module arrangement;

added maps, map_list, lift, lifts;

added stack.ML;

added simple_fact; generalized no_attributes;

Seq.maps;

added hide_names(_i) (from isar_thy.ML);

added generic_setup, add_oracle (from isar_thy.ML);

added exception EXCEPTION of exn * string;

replaced DATA_FAIL by EXCEPTION;

tuned Isar interfaces; tuned IsarThy.theorem_i;

added General/stack.ML, Isar/proof_display.ML;

the_list (cf. Pure/library.ML);

tuned IsarThy.theorem_i;

fixed INST: has same semantic now as INST_TYPE for repetitions

list of constants and theorems whose names have been changed or merged

add header

added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging

updated to work with latest HOL-Complex

add file Hyperreal/transfer.ML

new implementation of transfer principle

removed clutter