isabelle: src/HOL/Library/Simps_Case_Conv.thy@87067698ae53 (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
69568 de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm Andreas Lochbihler parents: 67724 diff changeset	6	imports Case_Converter
67013 335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3); wenzelm parents: 63582 diff changeset	7	keywords "simps_of_case" "case_of_simps" :: thy_decl
67724 63e305429f8a tuned; wenzelm parents: 67013 diff changeset	8	abbrevs "simps_of_case" "case_of_simps" = ""
53426 92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	9	begin
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	10
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 69568 diff changeset	11	ML_file \<open>simps_case_conv.ML\<close>
53426 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	end

author	wenzelm
	Fri, 08 Jan 2021 15:13:23 +0100
changeset 73102	87067698ae53
parent 69605	a96320074298
permissions	-rw-r--r--