QuotMain.thy
Mon, 07 Dec 2009 14:00:36 +0100 Cezary Kaliszyk inj_repabs_tac handles Babs now.
Mon, 07 Dec 2009 12:14:25 +0100 Cezary Kaliszyk Fix of regularize for babs and proof of babs_rsp.
Mon, 07 Dec 2009 08:45:04 +0100 Cezary Kaliszyk QuotProd with product_quotient and a 3 respects and preserves lemmas.
Mon, 07 Dec 2009 02:34:24 +0100 Christian Urban simplified the regularize simproc
Mon, 07 Dec 2009 01:28:10 +0100 Christian Urban now simpler regularize_tac with added solver works
Mon, 07 Dec 2009 01:22:20 +0100 Christian Urban removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
Mon, 07 Dec 2009 00:07:23 +0100 Christian Urban fixed examples
Sun, 06 Dec 2009 23:32:27 +0100 Christian Urban working state again
Sun, 06 Dec 2009 13:41:42 +0100 Christian Urban added a theorem list for equivalence theorems
Sun, 06 Dec 2009 11:39:34 +0100 Christian Urban updated Isabelle and deleted mono rules
Sun, 06 Dec 2009 11:21:29 +0100 Christian Urban more tuning of the code
Sun, 06 Dec 2009 11:09:51 +0100 Christian Urban puting code in separate sections
Sun, 06 Dec 2009 06:58:24 +0100 Cezary Kaliszyk Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.
Sun, 06 Dec 2009 04:03:08 +0100 Christian Urban working on lambda_prs with examples; polished code of clean_tac
less more (0) -300 -100 -14 tip