*To*: "Tao Ma" <separable at gmail.com>*Subject*: Re: [isabelle] simple lemma in ring theory*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 19 Dec 2006 10:59:37 +0100*Cc*: 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>

Dear Tao,

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

declare dvd1_def [simp]

another question is, if in this example suppose first i try "by blast"andit 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?

Clemens

**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: [isabelle] "Knaster_Tarski" Theorem? in Proof General
- Previous by Thread: Re: [isabelle] simple lemma in ring theory
- Next by Thread: [isabelle] CADE 2007 call for papers
- 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