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

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

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

Adapted to changes in Finite_Set theory.

- Adapted to new inductive definition package
- More elegant proof of eta postponement theorem inspired
by Andreas Abel

Adapted to new inductive definition package.

Converted to predicate notation.

Adapted to changes in List theory.

- wfP has been moved to theory Wellfounded_Recursion
- Accessible part now works on predicates, hence accP is
no longer needed

Adapted to changes in Transitive_Closure theory.

Adapted to new inductive definition package.

Adapted to changes in Finite_Set theory.

Theorems for converting between wf and wfP are now declared
as hints.