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

Inductive characterization of wfrec combinator.

Transitive closure is now defined via "inductive".

Representing set for type nat is now defined via "inductive".

Inductive definitions are now introduced earlier in the theory hierarchy.

nat_diff_split_asm, for the assumptions

if_splits and split_if_asm

fixed the X-symbol syntax for lambda

the rest of integer division

X-symbols for set theory

X-symbols for ZF