lib: add `changed <m>` Eisbach method, for CHANGED ML combinator

2016-06-19 14:05:26 +10:00 · 2016-06-19 14:05:26 +10:00 · 71b71cd9d7
parent a70f0138df
commit 71b71cd9d7
1 changed files with 9 additions and 0 deletions
--- 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 =>