diff -r 7f35355df72e -r 0cf166548856 Quot/Examples/LFex.thy --- a/Quot/Examples/LFex.thy Mon Dec 07 15:18:44 2009 +0100 +++ b/Quot/Examples/LFex.thy Mon Dec 07 15:21:51 2009 +0100 @@ -180,6 +180,8 @@ where "perm_trm \ (perm::'x prm \ trm \ trm)" +end + (* TODO/FIXME: Think whether these RSP theorems are true. *) lemma kpi_rsp[quotient_rsp]: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry @@ -299,9 +301,8 @@ apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) done -print_quotients - end +