isabelle: src/HOL/Library/Simps_Case_Conv.thy@73939a9b70a3 (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" = ""
53426 92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	11	begin
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	12
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	13	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	14
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	15	end

author	wenzelm
	Tue, 02 Aug 2016 17:35:18 +0200
changeset 63579	73939a9b70a3
parent 63432	ba7901e94e7b
child 63582	161c5d8ae266
permissions	-rw-r--r--