isabelle: src/HOL/Fun_Def_Base.thy@c103358a5559 (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
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain blanchet parents: diff changeset	11	ML_file "Tools/Function/function_lib.ML"
57959 1bfed12a7646 updated to named_theorems; wenzelm parents: 55968 diff changeset	12	named_theorems termination_simp "simplification rules for termination proofs"
55085 0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain blanchet parents: diff changeset	13	ML_file "Tools/Function/function_common.ML"
58816 aab139c0003f modernized setup; wenzelm parents: 57959 diff changeset	14	ML_file "Tools/Function/function_context_tree.ML"
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
55968 94242fa87638 tuning blanchet parents: 55085 diff changeset	20	ML_file "Tools/Function/sum_tree.ML"
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	wenzelm
	Wed, 17 May 2017 13:47:19 +0200
changeset 65851	c103358a5559
parent 60758	d8d85a8172b5
child 69605	a96320074298
permissions	-rw-r--r--