Re: [isabelle] help



jwang whu.edu.cn (jwang) wrote:
>   hello,
>    Apply(simp) or by auto often is used to  prove some  theorems automatically,so we can not see the process of simplication and we only see the result of simplication.How to  show the simplification process in Proof-General ,for example the rewrite rules used by the current simplification? Is there the command?
>                                                                          thanks
>                                                                            Jean

Select in ProofGeneral menu: Isabelle -> Settings -> Trace simplifier
Attention!  Output is verbose.

Note that you may also do single-step rewrites using the "unfold" and
"subst" methods and the "unfolding" keyword.  See Isar Reference manual.

	Florian
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.