*Subject*: Re: [isabelle] Blast behaves strangely with free schematic variables*From*: Peter <views at gmx.de>*Date*: Sun, 19 Feb 2006 11:36:51 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200602181614.k1IGE3j3030561@lobus.fungible.com>*References*: <200602181614.k1IGE3j3030561@lobus.fungible.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20051007 Debian/1.7.12-1

Tim Freeman wrote:

I downloaded Isabelle2005 just now following the installation instructions at http://www.cl.cam.ac.uk/Research/HVG/Isabelle/installation.html and if I start my "ToyList.thy" file with theory ToyList imports PreList begin lemma bug: "?A & ?B & ?XYZZY \<longrightarrow> ?XYZZY" by blast and go to the end and press control-c control-enter, I see this in the response window: lemma bug: ?A & ?B & gcd (?m, ?n) dvd ?n --> gcd (?m, ?n) dvd ?n I had expected it to say: lemma bug: ?A & ?B & ?XYZZY --> ?XYZZY I was surprised by the intruction of the "gcd" operator. If I change "blast" to "auto", I do get the output I expected.

I'm getting similiar results, with Main imported instead of PreList: theory Scratch imports Main begin lemma bug: "?A & ?B & ?XYZZY --> ?XYZZY" by blast outputs: lemma bug: ?A & ?B & [] \<in> lists ?Aa --> [] \<in> lists ?Aa

**Follow-Ups**:**Re: [isabelle] Blast behaves strangely with free schematic variables***From:*Tjark Weber

**References**:**[isabelle] Blast behaves strangely with free schematic variables***From:*Tim Freeman

- Previous by Date: [isabelle] Blast behaves strangely with free schematic variables
- Next by Date: Re: [isabelle] Blast behaves strangely with free schematic variables
- Previous by Thread: [isabelle] Blast behaves strangely with free schematic variables
- Next by Thread: Re: [isabelle] Blast behaves strangely with free schematic variables
- 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