*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Metalogical "spec" not resolved automatically*From*: Nicole Rauch <rauch at informatik.uni-kl.de>*Date*: Wed, 19 Oct 2005 10:20:11 +0200

Hello Isabelle-users,

1. !! N. [| 0 < N; P N |] ==> P (Suc 0) 2. !! N. [| 0 < N; P N; 0 < M |] ==> P M

Thanks for any insights Nicole

goal (show, 2 subgoals):

variables: P :: (nat \<Rightarrow> bool) M :: nat

**Attachment:
PGP.sig**

**Follow-Ups**:**Re: [isabelle] Metalogical "spec" not resolved automatically***From:*Stephan Merz

**Re: [isabelle] Metalogical "spec" not resolved automatically***From:*Alexander Krauss

**Re: [isabelle] Metalogical "spec" not resolved automatically***From:*Lawrence Paulson

**Re: [isabelle] Metalogical "spec" not resolved automatically***From:*Tjark Weber

- Previous by Date: Re: [isabelle] recdef tuple for 2 args, infix syntax possible?
- Next by Date: Re: [isabelle] Metalogical "spec" not resolved automatically
- Previous by Thread: Re: [isabelle] recdef tuple for 2 args, infix syntax possible?
- Next by Thread: Re: [isabelle] Metalogical "spec" not resolved automatically
- Cl-isabelle-users October 2005 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