*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] How to show that locale loop is finite?*From*: Victor Porton <porton at narod.ru>*Date*: Wed, 05 Jan 2011 01:31:38 +0300*Envelope-from*: porton@yandex.ru

The following theory does not verify. Which additional lemmas it needs to make it to verify? Isabelle does not understand that F(x) = x. How to make it to understand? theory test imports Main_ZF begin definition fdef: "F(x) == x" locale loc1 = fixes s1::i locale loc2 = fixes s2::i sublocale loc1 < p1: loc2 "F(s2)" . sublocale loc2 < p2: loc1 "F(s1)" . locale test = loc1 "0" interpretation inter: loc1 "0" sorry

**Follow-Ups**:**Re: [isabelle] How to show that locale loop is finite?***From:*Tobias Nipkow

**Re: [isabelle] How to show that locale loop is finite?***From:*Clemens Ballarin

- Previous by Date: [isabelle] Locale internal assumptions
- Next by Date: [isabelle] Using abbreviations with case expressions
- Previous by Thread: Re: [isabelle] Locale internal assumptions
- Next by Thread: Re: [isabelle] How to show that locale loop is finite?
- Cl-isabelle-users January 2011 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