| author | noschinl |
| Fri, 06 Sep 2013 10:56:40 +0200 | |
| changeset 53426 | 92db671e0ac6 |
| child 53433 | 3b356b7f7cad |
| permissions | -rw-r--r-- |
|
53426
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Simps_Case_Conv.thy |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
2 |
Author: Lars Noschinski |
|
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 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
7 |
keywords "simps_of_case" "case_of_simps" :: thy_decl |
|
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 |