321 (case (bare_concl goal) of |
321 (case (bare_concl goal) of |
322 (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) |
322 (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) |
323 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
323 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
324 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
324 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
325 |
325 |
|
326 | Const (@{const_name "op ="},_) $ |
|
327 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
328 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
329 rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1} |
|
330 |
|
331 (* TODO: Check why less _ are needed then in EX/ALL cases *) |
|
332 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
333 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ |
|
334 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) |
|
335 rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
336 |
326 (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) |
337 (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) |
327 | (Const (@{const_name "op ="},_) $ |
338 | (Const (@{const_name "op ="},_) $ |
328 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
339 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
329 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
340 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
330 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
341 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |