src/HOL/FunDef.thy
changeset 47432 e1576d13e933
parent 46950 d0181abdbdac
child 47701 157e6108a342
     1.1 --- a/src/HOL/FunDef.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -110,14 +110,21 @@
     1.4  use "Tools/Function/relation.ML"
     1.5  use "Tools/Function/function.ML"
     1.6  use "Tools/Function/pat_completeness.ML"
     1.7 +
     1.8 +method_setup pat_completeness = {*
     1.9 +  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
    1.10 +*} "prove completeness of datatype patterns"
    1.11 +
    1.12  use "Tools/Function/fun.ML"
    1.13  use "Tools/Function/induction_schema.ML"
    1.14  
    1.15 +method_setup induction_schema = {*
    1.16 +  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
    1.17 +*} "prove an induction principle"
    1.18 +
    1.19  setup {* 
    1.20    Function.setup
    1.21 -  #> Pat_Completeness.setup
    1.22    #> Function_Fun.setup
    1.23 -  #> Induction_Schema.setup
    1.24  *}
    1.25  
    1.26  subsection {* Measure Functions *}
    1.27 @@ -137,6 +144,12 @@
    1.28  by (rule is_measure_trivial)
    1.29  
    1.30  use "Tools/Function/lexicographic_order.ML"
    1.31 +
    1.32 +method_setup lexicographic_order = {*
    1.33 +  Method.sections clasimp_modifiers >>
    1.34 +  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
    1.35 +*} "termination prover for lexicographic orderings"
    1.36 +
    1.37  setup Lexicographic_Order.setup 
    1.38  
    1.39