*To*: Tao Ma <separable at gmail.com>*Subject*: Re: [isabelle] simple lemma in ring theory*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 19 Dec 2006 09:22:04 +0100*Cc*: Clemens Ballarin <ballarin at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <000401c722f1$c51ccc10$8202a8c0@babawu>*References*: <50f87d9a0612141801l4b3a7d32w32b6c1b2a04c4692@mail.gmail.com> <59c4f812542d7b85f9e9d4fd3635b1ec@in.tum.de> <000401c722f1$c51ccc10$8202a8c0@babawu>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

if i need to use this definition a lot, is it possible to modify theprover so that it willdo the unfold automatically?

You can tell the simplifier to use it every time by saying declare dvd1_def [simp]

another question is, if in this example suppose first i try "by blast" and it says "empty result sequence", how can i know that i need to add(unfold dvd1_def). is there a way to make the error message moremeaningful?basically what i would like to know is how far the automatic prover hasreached sothat i can add what's missing.

Tobias

**References**:**[isabelle] simple lemma in ring theory***From:*Tao Ma

**Re: [isabelle] simple lemma in ring theory***From:*Clemens Ballarin

**Re: [isabelle] simple lemma in ring theory***From:*Tao Ma

- Previous by Date: Re: [isabelle] simple lemma in ring theory
- Next by Date: Re: [isabelle] simple lemma in ring theory
- Previous by Thread: Re: [isabelle] simple lemma in ring theory
- Next by Thread: Re: [isabelle] simple lemma in ring theory
- Cl-isabelle-users December 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