summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Removed comment.

tuned;

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.