src/HOL/Tools/Function/context_tree.ML
changeset 55085 0e8e4dc55866
parent 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Function/context_tree.ML	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -35,6 +35,8 @@
     1.4  
     1.5    val rewrite_by_tree : Proof.context -> term -> thm -> (thm * thm) list ->
     1.6      ctx_tree -> thm * (thm * thm) list
     1.7 +
     1.8 +  val setup : theory -> theory
     1.9  end
    1.10  
    1.11  structure Function_Ctx_Tree : FUNCTION_CTXTREE =
    1.12 @@ -286,4 +288,8 @@
    1.13      rewrite_help [] [] x tr
    1.14    end
    1.15  
    1.16 +val setup =
    1.17 +  Attrib.setup @{binding fundef_cong} (Attrib.add_del cong_add cong_del)
    1.18 +    "declaration of congruence rule for function definitions"
    1.19 +
    1.20  end