isabelle: src/HOL/Library/Simps_Case_Conv.thy@4fa3e63ecc7e (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
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
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	11	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	12
92db671e0ac6 added simps_of_case and case_of_simps to convert between simps and case rules noschinl parents: diff changeset	13	end

author	paulson <lp15@cam.ac.uk>
	Sun, 06 May 2018 11:33:40 +0100
changeset 68095	4fa3e63ecc7e
parent 67724	63e305429f8a
child 69568	de09a7261120
permissions	-rw-r--r--