*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] Defines in locales in Isabelle 2009*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Wed, 22 Apr 2009 19:07:55 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <49EDB4D1.4020306@ipd.info.uni-karlsruhe.de>*References*: <49EDB4D1.4020306@ipd.info.uni-karlsruhe.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Quoting Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>:

locale foo = fixes x :: "'a => 'a => bool" and y :: "'a => 'a => bool" and P :: "'a => bool" and xs :: "'a => 'a => bool" ("_ ->* _") defines xs_def: "xs == (%a b. x a b & y a b)^**" assumes "a ->* b ==> P b" interpretation f: foo["%a b. a > 0 & b <= Suc 0" "%a b. a < 10" "%a.True"]

2nd try: interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10" "%a. True" "(%a b. a > 0 & b <= Suc 0 & a < 10)^**" Now the explicit parameter is given, but unfold_locales nor intro_locales longer work any longer (empty result sequence).

Clemens

**Follow-Ups**:**Re: [isabelle] Defines in locales in Isabelle 2009***From:*Brian Huffman

**References**:**[isabelle] Defines in locales in Isabelle 2009***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Porting trouble: Interpretation of locale semiring_1
- Next by Date: Re: [isabelle] Porting trouble: Interpretation of locale semiring_1
- Previous by Thread: [isabelle] Defines in locales in Isabelle 2009
- Next by Thread: Re: [isabelle] Defines in locales in Isabelle 2009
- Cl-isabelle-users April 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