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

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

X-symbols for ZF

X-symbols for set theory