--- a/src/HOL/FunDef.thy Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/FunDef.thy Thu Apr 12 18:39:19 2012 +0200
@@ -110,14 +110,21 @@
use "Tools/Function/relation.ML"
use "Tools/Function/function.ML"
use "Tools/Function/pat_completeness.ML"
+
+method_setup pat_completeness = {*
+ Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
+*} "prove completeness of datatype patterns"
+
use "Tools/Function/fun.ML"
use "Tools/Function/induction_schema.ML"
+method_setup induction_schema = {*
+ Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
+*} "prove an induction principle"
+
setup {*
Function.setup
- #> Pat_Completeness.setup
#> Function_Fun.setup
- #> Induction_Schema.setup
*}
subsection {* Measure Functions *}
@@ -137,6 +144,12 @@
by (rule is_measure_trivial)
use "Tools/Function/lexicographic_order.ML"
+
+method_setup lexicographic_order = {*
+ Method.sections clasimp_modifiers >>
+ (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
+*} "termination prover for lexicographic orderings"
+
setup Lexicographic_Order.setup