equal
deleted
inserted
replaced
100 qed "cut_apply"; |
100 qed "cut_apply"; |
101 |
101 |
102 (*** is_recfun ***) |
102 (*** is_recfun ***) |
103 |
103 |
104 goalw WF.thy [is_recfun_def,cut_def] |
104 goalw WF.thy [is_recfun_def,cut_def] |
105 "!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = (@z.True)"; |
105 "!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary"; |
106 by (etac ssubst 1); |
106 by (etac ssubst 1); |
107 by (asm_simp_tac HOL_ss 1); |
107 by (asm_simp_tac HOL_ss 1); |
108 qed "is_recfun_undef"; |
108 qed "is_recfun_undef"; |
109 |
109 |
110 (*** NOTE! some simplifications need a different finish_tac!! ***) |
110 (*** NOTE! some simplifications need a different finish_tac!! ***) |