src/HOL/Fun_Def_Base.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 60758 d8d85a8172b5
child 69605 a96320074298
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
blanchet@55085
     1
(*  Title:      HOL/Fun_Def_Base.thy
blanchet@55085
     2
    Author:     Alexander Krauss, TU Muenchen
blanchet@55085
     3
*)
blanchet@55085
     4
wenzelm@60758
     5
section \<open>Function Definition Base\<close>
blanchet@55085
     6
blanchet@55085
     7
theory Fun_Def_Base
blanchet@55085
     8
imports Ctr_Sugar Set Wellfounded
blanchet@55085
     9
begin
blanchet@55085
    10
blanchet@55085
    11
ML_file "Tools/Function/function_lib.ML"
wenzelm@57959
    12
named_theorems termination_simp "simplification rules for termination proofs"
blanchet@55085
    13
ML_file "Tools/Function/function_common.ML"
wenzelm@58816
    14
ML_file "Tools/Function/function_context_tree.ML"
wenzelm@58816
    15
wenzelm@58816
    16
attribute_setup fundef_cong =
wenzelm@58816
    17
  \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
wenzelm@58816
    18
  "declaration of congruence rule for function definitions"
wenzelm@58816
    19
blanchet@55968
    20
ML_file "Tools/Function/sum_tree.ML"
blanchet@55085
    21
blanchet@55085
    22
end