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" ..

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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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