author | wenzelm |
Tue, 02 Aug 2016 18:13:24 +0200 | |
changeset 63582 | 161c5d8ae266 |
parent 63579 | 73939a9b70a3 |
child 67013 | 335a7dce7cb3 |
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 |
7 |
keywords |
|
63579 | 8 |
"simps_of_case" "case_of_simps" :: thy_decl |
9 |
abbrevs |
|
10 |
"simps_of_case" = "" |
|
63582 | 11 |
"case_of_simps" = "" |
53426
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
12 |
begin |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
13 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
14 |
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
|
15 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
16 |
end |