Nominal/nominal_inductive.ML
Mon, 18 Apr 2011 15:56:07 +0100 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
Wed, 13 Apr 2011 13:41:52 +0100 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
less more (0) -2 tip