equal
deleted
inserted
replaced
364 mk_solver "distinctFieldSolver" (distinctTree_tac names); |
364 mk_solver "distinctFieldSolver" (distinctTree_tac names); |
365 |
365 |
366 fun distinct_simproc names = |
366 fun distinct_simproc names = |
367 Simplifier.make_simproc \<^context> |
367 Simplifier.make_simproc \<^context> |
368 {name = "DistinctTreeProver.distinct_simproc", |
368 {name = "DistinctTreeProver.distinct_simproc", |
|
369 kind = Simproc, |
369 lhss = [\<^term>\<open>x = y\<close>], |
370 lhss = [\<^term>\<open>x = y\<close>], |
370 proc = fn _ => fn ctxt => fn ct => |
371 proc = fn _ => fn ctxt => fn ct => |
371 (case Thm.term_of ct of |
372 (case Thm.term_of ct of |
372 Const (\<^const_name>\<open>HOL.eq\<close>, _) $ x $ y => |
373 Const (\<^const_name>\<open>HOL.eq\<close>, _) $ x $ y => |
373 Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) |
374 Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) |