Here is a sequence of actions with ProofPower which is causing me puzzlement.
:) set_merge_pcs ["unalg", "'latt2"]; val it = () : unit :) add_%exists%_cd_thms [MkLat_recursion_lemma] "'latt2"; val it = () : unit :) set_merge_pcs ["unalg", "'latt2"]; Exception Fail * Element cannot be found in list [find.1004] * raised So 'latt2 now seems to be in a mess. The theorem I used was like this (something similar worked previously). MkLat_recursion_lemma ; val it = %turnstile% %forall% cf C a b· %exists% f· f (MkLat C a b) = cf C a b : THM (it isn't really a recursion theorem, I just want to be able to write function definitions by pattern matching on MkLat). Any ideas on what is going on here? Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
