equal
deleted
inserted
replaced
20 (* -------------- step case ---------------- *) |
20 (* -------------- step case ---------------- *) |
21 by (REPEAT (rtac allI 1)); |
21 by (REPEAT (rtac allI 1)); |
22 by (rtac imp_conj_lemma 1); |
22 by (rtac imp_conj_lemma 1); |
23 by (simp_tac (simpset() addsimps [trans_of_def, |
23 by (simp_tac (simpset() addsimps [trans_of_def, |
24 C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); |
24 C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); |
|
25 by (induct_tac "a" 1); |
25 by (simp_tac (simpset() addsimps [h_abs_def]) 1); |
26 by (simp_tac (simpset() addsimps [h_abs_def]) 1); |
26 by (induct_tac "a" 1); |
|
27 by Auto_tac; |
|
28 qed"h_abs_is_abstraction"; |
27 qed"h_abs_is_abstraction"; |
29 |
28 |
30 |
29 |
31 (* |
30 (* |
32 Goalw [xt2_def,plift,option_lift] |
31 Goalw [xt2_def,plift,option_lift] |