author | wenzelm |
Mon, 12 Apr 2021 14:14:47 +0200 | |
changeset 73563 | 55b66a45bc94 |
parent 69605 | a96320074298 |
permissions | -rw-r--r-- |
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 | 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 | 11 |
ML_file \<open>Tools/Function/function_lib.ML\<close> |
57959 | 12 |
named_theorems termination_simp "simplification rules for termination proofs" |
69605 | 13 |
ML_file \<open>Tools/Function/function_common.ML\<close> |
14 |
ML_file \<open>Tools/Function/function_context_tree.ML\<close> |
|
58816 | 15 |
|
16 |
attribute_setup fundef_cong = |
|
17 |
\<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close> |
|
18 |
"declaration of congruence rule for function definitions" |
|
19 |
||
69605 | 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 |