equal
deleted
inserted
replaced
83 (Thm.trivial ct)) |
83 (Thm.trivial ct)) |
84 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
84 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
85 (* The result of the quantifier elimination *) |
85 (* The result of the quantifier elimination *) |
86 val (th, tac) = case prop_of pre_thm of |
86 val (th, tac) = case prop_of pre_thm of |
87 Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
87 Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
88 let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1) |
88 let val pth = linr_oracle (ctxt, Envir.eta_long [] t1) |
89 in |
89 in |
90 (trace_msg ("calling procedure with term:\n" ^ |
90 (trace_msg ("calling procedure with term:\n" ^ |
91 Syntax.string_of_term ctxt t1); |
91 Syntax.string_of_term ctxt t1); |
92 ((pth RS iffD2) RS pre_thm, |
92 ((pth RS iffD2) RS pre_thm, |
93 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
93 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |