isabelle: src/HOL/Library/Simps_Case_Conv.thy@3b356b7f7cad (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
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	7	keywords "simps_of_case" "case_of_simps" :: thy_decl
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 Sep 2013 12:05:01 +0200
changeset 53433	3b356b7f7cad
parent 53426	92db671e0ac6
child 56361	9f9f60f4dbbf
permissions	-rw-r--r--