equal
deleted
inserted
replaced
51 let |
51 let |
52 fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u; |
52 fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u; |
53 fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True}); |
53 fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True}); |
54 fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False}); |
54 fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False}); |
55 |
55 |
56 val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes; |
56 val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global o Drule.zero_var_indexes; |
57 |
57 |
58 fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs); |
58 fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs); |
59 fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)]; |
59 fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)]; |
60 |
60 |
61 val triv_inject_goals = |
61 val triv_inject_goals = |