[isabelle-dev] NEWS: method facts

Makarius makarius at sketis.net
Wed Jun 8 19:46:00 CEST 2016

*** Isar ***

* Proof methods may refer to the main facts via the dynamic fact
"method_facts". This is particularly useful for Eisbach method

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


More information about the isabelle-dev mailing list