QuotScript.thy
Sat, 24 Oct 2009 08:09:09 +0200 cek Better tactic and simplified the proof further
Fri, 23 Oct 2009 16:01:13 +0200 Cezary Kaliszyk eqsubst_tac
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
less more (0) -10 -7 tip