isabelle: src/HOL/Library/Simps_Case_Conv.thy@291934bac95e (annotated)

53433 3b356b7f7cad more standard header; wenzelm parents: 53426 diff changeset	1	(* Title: HOL/Library/Simps_Case_Conv.thy
3b356b7f7cad more standard header; wenzelm parents: 53426 diff changeset	2	Author: Lars Noschinski
53426 92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	3	*)
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	4
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	5	theory Simps_Case_Conv
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	6	imports Main
56361 9f9f60f4dbbf suppress slightly odd completion of "simp"; wenzelm parents: 53433 diff changeset	7	keywords "simps_of_case" :: thy_decl == "" and "case_of_simps" :: thy_decl
53426 92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	8	begin
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	9
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	10	ML_file "simps_case_conv.ML"
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	11
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	12	end

author	wenzelm
	Fri, 06 Mar 2015 15:58:56 +0100
changeset 59621	291934bac95e
parent 56361	9f9f60f4dbbf
child 63432	ba7901e94e7b
permissions	-rw-r--r--