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

Improved detection of identical clauses, also in the conjecture

Refinements to abstraction. Seeding with combinators K, I and B.

examples for hex and bin numerals

Changed and removed some functions related to combinators, since they are Isabelle constants now.

Now the DFG output includes correct declarations of c_fequal, but not hEXTENT

improvements to abstraction, ensuring more re-use of abstraction functions
moving some functions to Pure/drule.ML

facts about combinators

a few new functions on thms and cterms

reorganize and speed up termdiffs proofs

fixed bug in linear arith