src/HOL/Fun_Def_Base.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 60758 d8d85a8172b5
child 69605 a96320074298
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
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