Re: [isabelle] Printing instantiations



Hi Steve,

how automated proof tools actually accomplish the proof is somehow
magic; if you want to specify single proof steps explicitly, restrict
yourself to proper Isar proofs with methods rule, default etc., see also
the tutorial on Isar.  For your example, this could read e.g.

definition c :: real where
  ax1: "c = 0"

lemma test: "EX x::real. x = 0"
proof -
  from ax1 show "EX x::real. x = 0" ..
qed

Note also that auto won't ever use ax1 in your proof: you need a type
constraint on the existential x, otherwise ax1 is not sufficient.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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