author | haftmann |
Tue, 21 Apr 2020 07:28:17 +0000 | |
changeset 71788 | ca3ac5238c41 |
parent 69605 | a96320074298 |
permissions | -rw-r--r-- |
53433 | 1 |
(* Title: HOL/Library/Simps_Case_Conv.thy |
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 | 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 | 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 |