| changeset 9108 | 9fff97d29837 |
| parent 7293 | 959e060f4a2f |
| child 11954 | 3d1780208bf3 |
--- a/src/HOL/Datatype.ML Thu Jun 22 11:37:13 2000 +0200 +++ b/src/HOL/Datatype.ML Thu Jun 22 23:04:34 2000 +0200 @@ -8,6 +8,8 @@ (*compatibility*) val [sum_case_Inl, sum_case_Inr] = sum.cases; +bind_thm ("sum_case_Inl", sum_case_Inl); +bind_thm ("sum_case_Inr", sum_case_Inr); Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; by (EVERY1 [res_inst_tac [("s","s")] sumE,