--- a/src/HOL/Library/BNF_Corec.thy Mon Oct 24 16:16:55 2016 +0200
+++ b/src/HOL/Library/BNF_Corec.thy Mon Oct 24 16:53:32 2016 +0200
@@ -206,6 +206,10 @@
ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
+method_setup transfer_prover_eq = \<open>
+ Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
+\<close> "apply transfer_prover after folding relator_eq"
+
method_setup corec_unique = \<open>
Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
\<close> "prove uniqueness of corecursive equation"