Re: [isabelle] discarding an assumption


On Tue, Nov 20, 2007 at 05:03:23AM +0000, Dave Cunningham wrote:
> Is it possible to delete an assumption from the current subgoal?

  There is thin_tac, describe in Section 3.3.2 "Manipulating
assumptions" of the Isabelle Reference Manual (-> isatool doc ref).

  Best regards,


Dr. Mark A. Hillebrand
German Research Center for Artificial Intelligence
Saarbruecken, Germany
Building E1 1, Room 4.06
Phone: +49 (0)681 302 57379    Fax: +49 (0)681 302 4290
Email: mah at

Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
Trippstadter Strasse 122, D-67663 Kaiserslautern, Germany

Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313

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