src/HOL/Fun_Def_Base.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 60758 d8d85a8172b5
child 69605 a96320074298
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
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