author | haftmann |
Sat, 28 Jun 2014 21:09:17 +0200 | |
changeset 57427 | 91f9e4148460 |
parent 56361 | 9f9f60f4dbbf |
child 63432 | ba7901e94e7b |
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 |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
6 |
imports Main |
56361 | 7 |
keywords "simps_of_case" :: thy_decl == "" and "case_of_simps" :: thy_decl |
53426
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
8 |
begin |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
9 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
10 |
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
|
11 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
12 |
end |