author | huffman |
Fri, 03 Jun 2005 23:35:18 +0200 | |
changeset 16216 | 279ab2e02089 |
parent 16215 | 7ff978ca1920 |
child 16217 | 96f0c8546265 |
--- a/src/HOLCF/Lift.thy Fri Jun 03 23:34:49 2005 +0200 +++ b/src/HOLCF/Lift.thy Fri Jun 03 23:35:18 2005 +0200 @@ -247,7 +247,7 @@ cont (%y. lift_case UU (f y) (g y))" -- {* @{text flift1} is continuous in a variable that occurs either in the @{text Def} branch or in the argument. *} - apply (rule_tac tt = g in cont2cont_app) + apply (rule_tac t=g in cont2cont_app) apply (rule cont_flift1_not_arg) apply auto apply (rule cont_flift1_arg)