QuotMain.thy
2009-11-04 Christian Urban separated the quotient_def into a separate file
2009-11-04 Christian Urban fixed definition of PLUS
2009-11-04 Christian Urban simplified the quotient_def code
2009-11-04 Cezary Kaliszyk Lifting 'fold1.simps(2)' and some cleaning.
2009-11-03 Cezary Kaliszyk merge
2009-11-03 Cezary Kaliszyk applic_prs
2009-11-03 Christian Urban simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
2009-11-03 Cezary Kaliszyk Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
2009-11-02 Christian Urban split quotient.ML into two files
2009-11-02 Christian Urban slightly saner way of parsing the quotient_def
2009-11-02 Christian Urban changed Type.typ_match to Sign.typ_match
2009-11-02 Cezary Kaliszyk Optimization
2009-11-02 Cezary Kaliszyk Fixed quotdata_lookup.
2009-11-02 Christian Urban merged
2009-11-02 Christian Urban fixed the problem with types in map
2009-10-31 Cezary Kaliszyk Automatic computation of application preservation and manually finished "alpha.induct". Slow...
2009-10-30 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts.
2009-10-30 Cezary Kaliszyk Regularization
2009-10-30 Cezary Kaliszyk Finally merged the code of the versions of regularize and tested examples.
2009-10-30 Cezary Kaliszyk Finding applications and duplicates filtered out in abstractions
2009-10-30 Cezary Kaliszyk Cleaning of the interface to lift.
2009-10-29 Cezary Kaliszyk Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
2009-10-29 Cezary Kaliszyk Using subst for identity definition.
2009-10-28 Cezary Kaliszyk Fix also in the general procedure.
2009-10-28 Cezary Kaliszyk Fixes
2009-10-28 Christian Urban merged
2009-10-28 Christian Urban added infrastructure for defining lifted constants
2009-10-28 Cezary Kaliszyk First experiments with Lambda
2009-10-28 Cezary Kaliszyk Proof of append_rsp
2009-10-28 Christian Urban merged
less more (0) -100 -50 -30 tip