equal
deleted
inserted
replaced
83 (* The result of the quantifier elimination *) |
83 (* The result of the quantifier elimination *) |
84 val (th, tac) = |
84 val (th, tac) = |
85 (case Thm.prop_of pre_thm of |
85 (case Thm.prop_of pre_thm of |
86 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
86 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
87 let |
87 let |
88 val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1)) |
88 val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1) |
89 in |
89 in |
90 ((pth RS iffD2) RS pre_thm, |
90 ((pth RS iffD2) RS pre_thm, |
91 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
91 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
92 end |
92 end |
93 | _ => (pre_thm, assm_tac i)) |
93 | _ => (pre_thm, assm_tac i)) |