356 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
356 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
357 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ |
357 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ |
358 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) |
358 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) |
359 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
359 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
360 |
360 |
|
361 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
362 (Const(@{const_name Bexeq},_) $ _) $ (Const(@{const_name Bexeq},_) $ _) |
|
363 => rtac @{thm bexeq_rsp} THEN' quotient_tac ctxt |
|
364 |
361 | (_ $ |
365 | (_ $ |
362 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
366 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
363 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
367 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
364 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
368 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
365 |
369 |