isabelle: src/HOL/Fun_Def_Base.thy@c0587d661ea8 (annotated)

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

author	paulson <lp15@cam.ac.uk>
	Fri, 02 May 2025 16:25:38 +0100
changeset 82595	c0587d661ea8
parent 69605	a96320074298
permissions	-rw-r--r--