equal
deleted
inserted
replaced
89 TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)] |
89 TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)] |
90 (Thm.trivial ct)) |
90 (Thm.trivial ct)) |
91 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
91 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
92 (* The result of the quantifier elimination *) |
92 (* The result of the quantifier elimination *) |
93 val (th, tac) = case prop_of pre_thm of |
93 val (th, tac) = case prop_of pre_thm of |
94 Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ => |
94 Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
95 let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1) |
95 let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1) |
96 in |
96 in |
97 (trace_msg ("calling procedure with term:\n" ^ |
97 (trace_msg ("calling procedure with term:\n" ^ |
98 Syntax.string_of_term ctxt t1); |
98 Syntax.string_of_term ctxt t1); |
99 ((pth RS iffD2) RS pre_thm, |
99 ((pth RS iffD2) RS pre_thm, |