Nominal/nominal_dt_alpha.ML
Mon, 06 Dec 2010 14:24:17 +0000 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Fri, 03 Dec 2010 13:51:07 +0000 Christian Urban updated to Isabelle 2nd December
Sat, 13 Nov 2010 10:25:03 +0000 Christian Urban respectfulness for permute_bn functions
Fri, 12 Nov 2010 01:20:53 +0000 Christian Urban automated permute_bn functions (raw ones first)
Wed, 10 Nov 2010 13:46:21 +0000 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
Mon, 20 Sep 2010 21:52:45 +0800 Christian Urban introduced a general procedure for structural inductions; simplified reflexivity proof
Sun, 12 Sep 2010 22:46:40 +0800 Christian Urban tuned code
less more (0) -30 -10 -7 tip