removed begin; added global section; added global_names flag (tmp), default true;

fixed prep_ext;

Simplified proof.

Simplified proof because of better simplifier.

Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).

added transfer: theory -> thm -> thm;

oops;

The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.

fixed dependencies;

transfer thy Ord_nat;

sevaral goals restated in mono.thy;

moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;

transfer InfDatatype.thy Limit_VfromE;

transfer CardinalArith.thy nat_into_Ord;

improved pretty_arity;

added merge_theories (new name arg);

fixed merge_theories;

revert to 1.3;

revert to 1.1;

Added last, butlast, dropped ttl.

lala

Eta-expansion of function declarations, for value polymorphism

remove merge_theories; merge_list: always prepares extend -- no longer supports aliasing merges;

make_draft replaced by prep_ext; improved print_data; merge now does trivial (absorptive) merges only; added nontriv_merge;