equal
deleted
inserted
replaced
51 in |
51 in |
52 |
52 |
53 val lazy_conj_simproc = |
53 val lazy_conj_simproc = |
54 Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"] |
54 Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"] |
55 (fn thy => fn ss => fn t => |
55 (fn thy => fn ss => fn t => |
56 (case t of (Const (@{const_name "op &"},_)$P$Q) => |
56 (case t of (Const (@{const_name HOL.conj},_)$P$Q) => |
57 let |
57 let |
58 val P_P' = Simplifier.rewrite ss (cterm_of thy P); |
58 val P_P' = Simplifier.rewrite ss (cterm_of thy P); |
59 val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 |
59 val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 |
60 in if isFalse P' |
60 in if isFalse P' |
61 then SOME (conj1_False OF [P_P']) |
61 then SOME (conj1_False OF [P_P']) |