equal
deleted
inserted
replaced
409 | conjuncts_aux t conjs = t::conjs; |
409 | conjuncts_aux t conjs = t::conjs; |
410 |
410 |
411 fun conjuncts t = conjuncts_aux t []; |
411 fun conjuncts t = conjuncts_aux t []; |
412 |
412 |
413 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true |
413 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true |
414 | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true |
414 | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true |
415 | is_equationlike_term _ = false |
415 | is_equationlike_term _ = false |
416 |
416 |
417 val is_equationlike = is_equationlike_term o prop_of |
417 val is_equationlike = is_equationlike_term o prop_of |
418 |
418 |
419 fun is_pred_equation_term (Const ("==", _) $ u $ v) = |
419 fun is_pred_equation_term (Const ("==", _) $ u $ v) = |