equal
deleted
inserted
replaced
317 qed_goalw "beta_cfun_sprod" thy [spair_def] |
317 qed_goalw "beta_cfun_sprod" thy [spair_def] |
318 "(LAM x y. Ispair x y)`a`b = Ispair a b" |
318 "(LAM x y. Ispair x y)`a`b = Ispair a b" |
319 (fn prems => |
319 (fn prems => |
320 [ |
320 [ |
321 (stac beta_cfun 1), |
321 (stac beta_cfun 1), |
322 (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1, |
322 (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1, |
323 cont2cont_CF1L]) 1), |
323 cont2cont_CF1L]) 1), |
324 (stac beta_cfun 1), |
324 (stac beta_cfun 1), |
325 (rtac cont_Ispair2 1), |
325 (rtac cont_Ispair2 1), |
326 (rtac refl 1) |
326 (rtac refl 1) |
327 ]); |
327 ]); |