src/HOL/Fun_Def_Base.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 69605 a96320074298
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55085
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Fun_Def_Base.thy
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     2
    Author:     Alexander Krauss, TU Muenchen
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     3
*)
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     5
section \<open>Function Definition Base\<close>
55085
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     6
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     7
theory Fun_Def_Base
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     8
imports Ctr_Sugar Set Wellfounded
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
     9
begin
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
    10
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 60758
diff changeset
    11
ML_file \<open>Tools/Function/function_lib.ML\<close>
57959
1bfed12a7646 updated to named_theorems;
wenzelm
parents: 55968
diff changeset
    12
named_theorems termination_simp "simplification rules for termination proofs"
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 60758
diff changeset
    13
ML_file \<open>Tools/Function/function_common.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 60758
diff changeset
    14
ML_file \<open>Tools/Function/function_context_tree.ML\<close>
58816
aab139c0003f modernized setup;
wenzelm
parents: 57959
diff changeset
    15
aab139c0003f modernized setup;
wenzelm
parents: 57959
diff changeset
    16
attribute_setup fundef_cong =
aab139c0003f modernized setup;
wenzelm
parents: 57959
diff changeset
    17
  \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
aab139c0003f modernized setup;
wenzelm
parents: 57959
diff changeset
    18
  "declaration of congruence rule for function definitions"
aab139c0003f modernized setup;
wenzelm
parents: 57959
diff changeset
    19
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 60758
diff changeset
    20
ML_file \<open>Tools/Function/sum_tree.ML\<close>
55085
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
    21
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
diff changeset
    22
end