[isabelle] Fwd: Using smt_tac from ML



Dear all,

I would like to write a tactic that reproduces the following:

  apply(simp add: subset_iff)
  apply smt

I am applying this tactic to formulae like (EX s. C <= {s}) ⟹ (EX s. A Int
C <= {s})

So far, I got this:

  (TRY
    (full_simp_tac ((simpset_of ctxt) addsimps [ at {thm subset_iff}]) i) THEN
    (SMT_Solver.smt_tac ctxt [] i))

However, the smt_tac raises the following:

  exception Option raised (line 81 of "General/basics.ML") At command
"apply"

I believe I am not using smt_tac correctly. Could I ask for advice on how
to use smt_tac?

I am using Isabelle 2012.

Thank you very much for your help.

Kindest,
---
Matej



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.