FSet.thy
2009-12-03 Cezary Kaliszyk defs used automatically by clean_tac
2009-12-03 Cezary Kaliszyk Added the definition to quotient constant data.
2009-12-03 Cezary Kaliszyk removing unused code
2009-12-02 Christian Urban deleted now obsolete argument rty everywhere
2009-12-02 Cezary Kaliszyk Lifting to 2 different types :)
2009-12-02 Cezary Kaliszyk New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
2009-12-02 Cezary Kaliszyk Fixed unlam for non-abstractions and updated list_induct_part proof.
2009-12-02 Cezary Kaliszyk Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
2009-12-02 Cezary Kaliszyk The conversion approach works.
2009-12-02 Cezary Kaliszyk Trying a conversion based approach.
2009-12-02 Cezary Kaliszyk A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
2009-12-01 Cezary Kaliszyk back in working state
2009-12-01 Cezary Kaliszyk clean
2009-12-01 Christian Urban added a make_inst test
2009-12-01 Cezary Kaliszyk Transformation of QUOT_TRUE assumption by any given function
less more (0) -100 -15 tip