NEWS
changeset 60119 54bea620e54f
parent 60115 9a1c6587e6c1
child 60138 b11401808dac
child 60258 7364d4316a56
     1.1 --- a/NEWS	Fri Apr 17 16:54:25 2015 +0200
     1.2 +++ b/NEWS	Fri Apr 17 17:49:19 2015 +0200
     1.3 @@ -59,6 +59,13 @@
     1.4  * Structural composition of proof methods (meth1; meth2) in Isar
     1.5  corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
     1.6  
     1.7 +* The Eisbach proof method language allows to define new proof methods
     1.8 +by combining existing ones with their usual syntax. The "match" proof
     1.9 +method provides basic fact/term matching in addition to
    1.10 +premise/conclusion matching through Subgoal.focus, and binds fact names
    1.11 +from matches as well as term patterns within matches. See also
    1.12 +~~/src/HOL/Eisbach/Eisbach.thy and the included examples.
    1.13 +
    1.14  
    1.15  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.16