| changeset 9108 | 9fff97d29837 |
| parent 9014 | 4382883421ec |
| child 9187 | 68ecc04785f1 |
--- a/src/HOL/List.ML Thu Jun 22 11:37:13 2000 +0200 +++ b/src/HOL/List.ML Thu Jun 22 23:04:34 2000 +0200 @@ -32,7 +32,7 @@ by (REPEAT (ares_tac basic_monos 1)); qed "lists_mono"; -val listsE = lists.mk_cases "x#l : lists A"; +bind_thm ("listsE", lists.mk_cases "x#l : lists A"); AddSEs [listsE]; AddSIs lists.intrs;