equal
deleted
inserted
replaced
1 (* Title: Subst/AList.ML |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Association lists. |
|
7 *) |
|
8 |
|
9 open AList; |
|
10 |
|
11 val prems = goal AList.thy |
|
12 "[| P([]); \ |
|
13 \ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"; |
|
14 by (induct_tac "l" 1); |
|
15 by (split_all_tac 2); |
|
16 by (REPEAT (ares_tac prems 1)); |
|
17 qed "alist_induct"; |
|
18 |
|
19 (*Perform induction on xs. *) |
|
20 fun alist_ind_tac a M = |
|
21 EVERY [induct_thm_tac alist_induct a M, |
|
22 rename_last_tac a ["1"] (M+1)]; |
|