# HG changeset patch # User Cezary Kaliszyk # Date 1271751819 -7200 # Node ID 4fa94551eebc6ead5e2a785b53c18c077a988d42 # Parent 950fd9b8f05e4eac5dca8baa348157b528b05de9 Fix of comment diff -r 950fd9b8f05e -r 4fa94551eebc Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Apr 20 09:13:52 2010 +0200 +++ b/Nominal/Parser.thy Tue Apr 20 10:23:39 2010 +0200 @@ -331,7 +331,7 @@ Rsp.thy/prove_const_rsp 17) prove respects for all datatype constructors (unfold eq_iff and alpha_gen; introduce zero permutations; simp) -Lift.thy/quotient_lift_consts_export +Perm.thy/quotient_lift_consts_export 18) define lifted constructors, fv, bn, alpha_bn, permutations Perm.thy/define_lifted_perms 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass