# HG changeset patch # User kuncar # Date 1397144893 -7200 # Node ID 7e8a369eb10d36e250fa744a626c343289869a3c # Parent a13c2ccc160b7622642b0e0e38dd9bc4699df0e3 tuned diff -r a13c2ccc160b -r 7e8a369eb10d src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Thu Apr 10 15:14:38 2014 +0200 +++ b/src/HOL/Lifting.thy Thu Apr 10 17:48:13 2014 +0200 @@ -48,9 +48,9 @@ where "left_unique R \ (\x y z. R x z \ R y z \ x = y)" lemma left_unique_transfer [transfer_rule]: - assumes [transfer_rule]: "right_total A" - assumes [transfer_rule]: "right_total B" - assumes [transfer_rule]: "bi_unique A" + assumes "right_total A" + assumes "right_total B" + assumes "bi_unique A" shows "((A ===> B ===> op=) ===> implies) left_unique left_unique" using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def by metis