src/HOL/Library/BNF_Corec.thy
changeset 64378 e9eb0b99a44c
parent 62700 e3ca8dc01c4f
child 64379 71f42dcaa1df
     1.1 --- a/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:16:55 2016 +0200
     1.2 +++ b/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:53:32 2016 +0200
     1.3 @@ -206,6 +206,10 @@
     1.4  ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
     1.5  ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
     1.6  
     1.7 +method_setup transfer_prover_eq = \<open>
     1.8 +  Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
     1.9 +\<close> "apply transfer_prover after folding relator_eq"
    1.10 +
    1.11  method_setup corec_unique = \<open>
    1.12    Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
    1.13  \<close> "prove uniqueness of corecursive equation"