src/HOL/HOLCF/Fixrec.thy
changeset 47432 e1576d13e933
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -230,7 +230,9 @@
     1.4  use "Tools/holcf_library.ML"
     1.5  use "Tools/fixrec.ML"
     1.6  
     1.7 -setup {* Fixrec.setup *}
     1.8 +method_setup fixrec_simp = {*
     1.9 +  Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
    1.10 +*} "pattern prover for fixrec constants"
    1.11  
    1.12  setup {*
    1.13    Fixrec.add_matchers