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;