*To*: Tim Freeman <tim at fungible.com>*Subject*: Re: [isabelle] Blast behaves strangely with free schematic variables*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 19 Feb 2006 11:11:18 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200602181614.k1IGE3j3030561@lobus.fungible.com>*References*: <200602181614.k1IGE3j3030561@lobus.fungible.com>

Larry Paulson On 18 Feb 2006, at 15:07, Tim Freeman wrote:

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.

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

- Previous by Date: Re: [isabelle] Blast behaves strangely with free schematic variables
- Next by Date: Re: [isabelle] overloaded defs
- Previous by Thread: Re: [isabelle] Blast behaves strangely with free schematic variables
- Next by Thread: [isabelle] IJCAR 2006: Call For Papers (CFP)
- 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