*** Isar ***
* Proof methods may refer to the main facts via the dynamic fact
"method_facts". This is particularly useful for Eisbach method
definitions.
* Eisbach provides method "use" to modify the main facts of a given
method expression, e.g.
(use facts in simp)
(use facts in ‹simp add: ...›)
This refers to Isabelle/29fe61d5f748.
An example application is here in AFP:
changeset: 6764:1892b23de862
tag: tip
user: wenzelm
date: Wed Jun 08 19:41:05 2016 +0200
files: thys/Bell_Numbers_Spivey/Bell_Numbers.thy
description:
clarified handling of method_facts, like SIMPLE_METHOD;
There are further possibilities for "use", e.g. to eliminate auxiliary
"-" or "insert" steps, notably:
qed (insert a, auto) ~> qed (use a in auto)
The plan to support (use [[simproc a]] in simp) did not work out yet: I
need to rework the parsers for thms and attrib first.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
