From 71b71cd9d750af63c5d2ed0f26c54a853807220f Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@nicta.com.au>
Date: Sun, 19 Jun 2016 14:05:26 +1000
Subject: [PATCH] lib: add `changed <m>` Eisbach method, for CHANGED ML
 combinator

---
 lib/Eisbach_Methods.thy | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/lib/Eisbach_Methods.thy b/lib/Eisbach_Methods.thy
index ddbc39806..c016f91fd 100644
--- a/lib/Eisbach_Methods.thy
+++ b/lib/Eisbach_Methods.thy
@@ -60,6 +60,15 @@ method_setup determ =
 
    in SIMPLE_METHOD (DETERM tac) facts end)
 \<close>
+
+method_setup changed =
+ \<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
+   let
+     fun tac st' = method_evaluate m ctxt facts st'
+
+   in SIMPLE_METHOD (CHANGED tac) facts end)
+\<close>
+
  
 method_setup timeit =
  \<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>