equal
deleted
inserted
replaced
13 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
14 |
14 |
15 qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun" |
15 qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun" |
16 (fn prems => |
16 (fn prems => |
17 [ |
17 [ |
18 (rtac (mem_Collect_eq RS ssubst) 1), |
18 (stac mem_Collect_eq 1), |
19 (rtac cont_id 1) |
19 (rtac cont_id 1) |
20 ]); |
20 ]); |
21 |
21 |
22 |
22 |
23 (* ------------------------------------------------------------------------ *) |
23 (* ------------------------------------------------------------------------ *) |