*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] instance theorems*From*: Sean McLaughlin <seanmcl at cmu.edu>*Date*: Fri, 17 Feb 2006 16:41:12 -0500

Hello, How do you get at the theorems which prove the "instance" calls? Eg. the proof term for instance * :: (finite, finite) finite proof show "finite (UNIV :: ('a ◊ 'b) set)" proof (rule finite_Prod_UNIV) show "finite (UNIV :: 'a set)" by (rule finite) show "finite (UNIV :: 'b set)" by (rule finite) qed qed Thanks, Sean

- Previous by Date: Re: [isabelle] type mappings
- Next by Date: [isabelle] Blast behaves strangely with free schematic variables
- Previous by Thread: [isabelle] CFP: FCS-ARSPA'06 (Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis)
- Next by Thread: Re: [isabelle] instance theorems
- Cl-isabelle-users February 2006 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