Nominal/ExCoreHaskell.thy
Thu, 25 Mar 2010 17:30:46 +0100 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
Thu, 25 Mar 2010 14:31:51 +0100 Cezary Kaliszyk Showed ACons_subst.
Thu, 25 Mar 2010 14:24:06 +0100 Cezary Kaliszyk Only ACons_subst left to show.
Thu, 25 Mar 2010 12:04:38 +0100 Cezary Kaliszyk Solved all boring subgoals, and looking at properly defning permute_bv
Thu, 25 Mar 2010 11:29:54 +0100 Cezary Kaliszyk One more copy-and-paste in core-haskell.
Wed, 24 Mar 2010 18:02:33 +0100 Cezary Kaliszyk Further in the strong induction proof.
Wed, 24 Mar 2010 16:06:31 +0100 Cezary Kaliszyk Solved one of the strong-induction goals.
less more (0) -10 -7 tip