isabelle: src/HOL/Library/Simps_Case_Conv.thy@ad96222853fc (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
63432 ba7901e94e7b tuned; wenzelm parents: 56361 diff changeset	6	imports Main
ba7901e94e7b tuned; wenzelm parents: 56361 diff changeset	7	keywords
63579 73939a9b70a3 support 'abbrevs' within theory header; wenzelm parents: 63432 diff changeset	8	"simps_of_case" "case_of_simps" :: thy_decl
73939a9b70a3 support 'abbrevs' within theory header; wenzelm parents: 63432 diff changeset	9	abbrevs
73939a9b70a3 support 'abbrevs' within theory header; wenzelm parents: 63432 diff changeset	10	"simps_of_case" = ""
63582 161c5d8ae266 avoid confusion with 'case' and "cases"; wenzelm parents: 63579 diff changeset	11	"case_of_simps" = ""
53426 92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	12	begin
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	13
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	14	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	15
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	16	end

author	wenzelm
	Mon, 18 Sep 2017 18:26:55 +0200
changeset 66678	ad96222853fc
parent 63582	161c5d8ae266
child 67013	335a7dce7cb3
permissions	-rw-r--r--