*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] The problem restated*From*: Victor Porton <porton at narod.ru>*Date*: Sun, 15 Mar 2009 14:22:19 +0300

In the following theory the theorem ret_th1 verifies well but the theorem ret_th2 fails to verify. How this file could be changed to verify ret_th2 also? --- theory test imports Perm begin (*Should be replaced with actual definitions*) consts big::i consts newbig::i consts move::i theorem move_th: "move: bij(big, newbig)" sorry definition ret_def: "ret == converse(move)" theorem ret_th1: "converse(move): bij(newbig, big)" using move_th bij_converse_bij by simp; theorem ret_th2: "ret: bij(newbig, big)" using move_th bij_converse_bij by simp; end

**Follow-Ups**:**Re: [isabelle] The problem restated***From:*Brian Huffman

- Previous by Date: [isabelle] Second call for papers: Modules and Libraries for Proof Assistants
- Next by Date: [isabelle] How do I find out via "find_theorems", for an existing theorem, whether it is marked as simp/intro/elim?
- Previous by Thread: [isabelle] Second call for papers: Modules and Libraries for Proof Assistants
- Next by Thread: Re: [isabelle] The problem restated
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list