author | haftmann |
Thu, 08 Nov 2018 09:11:52 +0100 | |
changeset 69260 | 0a9688695a1b |
parent 67724 | 63e305429f8a |
child 69568 | de09a7261120 |
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 |
63432 | 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 | 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 |