*To*: David Streader <dstr at cs.waikato.ac.nz>*Subject*: Re: [isabelle] interpretations and *** exception Option raised*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 23 Sep 2008 13:07:44 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <48C6F4D2.5050700@cs.waikato.ac.nz>*References*: <48C6F4D2.5050700@cs.waikato.ac.nz>

Hi David,

Hi I am lost as to what is wrong! The last lemma (see below orattached for simplified theory) results in error:*** exception Option raised *** At command "lemma".but if the lemma is moved to line --"Lemma works here" thenthe error disapears.Have I made some silly mistake?

theory Except imports Main begin locale genr = fixes Ent :: "'a set"fixes Xi :: "'x set" fixes User :: "'a => 'x => (('atom)list) set"context genr begin definition Refeq :: "'a ^ 'a ^ bool" where "(Refeq a c) = (a = c)" end locale Pref = fixes PEntities :: "int set"fixes PXi :: "int set" fixes PUser :: "int => int => ((int)list)set"defines user: "PUser E X == {[E,X]}" --"Lemma works here" interpretation Pref < genr proof qed

interpretation Pref < gen PEntities PXi PUser proof qed Clemens

**References**:**[isabelle] interpretations and *** exception Option raised***From:*David Streader

- Previous by Date: Re: [isabelle] Partial definitions of datatypes
- Next by Date: [isabelle] Syntax for theory definitions
- Previous by Thread: Re: [isabelle] interpretations and *** exception Option raised
- Next by Thread: [isabelle] transitive closure
- Cl-isabelle-users September 2008 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