| changeset 48 | 21291189b51e |
| parent 40 | ac7b7003f177 |
| child 66 | 14b9286ed036 |
| 47:69d815b0e1eb | 48:21291189b51e |
|---|---|
335 |
335 |
336 fun stac th = rtac(th RS ssubst); |
336 fun stac th = rtac(th RS ssubst); |
337 fun sstac ths = EVERY' (map stac ths); |
337 fun sstac ths = EVERY' (map stac ths); |
338 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); |
338 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); |
339 |
339 |
340 |
|
340 end; |
341 end; |
341 |
342 |
342 open HOL_Lemmas; |
343 open HOL_Lemmas; |