equal
deleted
inserted
replaced
355 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
355 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
356 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
356 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
357 |
357 |
358 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
358 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
359 (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) |
359 (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) |
360 => rtac @{thm bexeq_rsp} THEN' quotient_tac ctxt |
360 => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt |
361 |
361 |
362 | (_ $ |
362 | (_ $ |
363 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
363 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
364 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
364 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
365 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
365 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |