QuotScript.thy
Thu, 22 Oct 2009 15:44:16 +0200 Cezary Kaliszyk Removed an assumption
Thu, 22 Oct 2009 15:02:01 +0200 Cezary Kaliszyk The proof now including manually unfolded higher-order RES_FORALL_RSP.
Thu, 22 Oct 2009 13:45:48 +0200 Cezary Kaliszyk The problems with 'abs' term.
Sat, 17 Oct 2009 16:06:54 +0200 Cezary Kaliszyk Partial simplification of the proof
Fri, 16 Oct 2009 17:05:52 +0200 Cezary Kaliszyk Symmetric version of REP_ABS_RSP
Fri, 16 Oct 2009 16:51:01 +0200 Cezary Kaliszyk Progressing with the proof
Thu, 15 Oct 2009 10:25:23 +0200 Cezary Kaliszyk A number of lemmas for REGULARIZE_TAC and regularizing card1.
less more (0) -7 tip