equal
deleted
inserted
replaced
90 (trivial ct)) |
90 (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 ("Trueprop", _) $ t1) $ _ => |
94 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
95 let val pth = linr_oracle (cterm_of thy (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, |
100 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
100 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |