equal
deleted
inserted
replaced
108 (Thm.trivial ct)) |
108 (Thm.trivial ct)) |
109 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
109 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
110 (* The result of the quantifier elimination *) |
110 (* The result of the quantifier elimination *) |
111 val (th, tac) = case (prop_of pre_thm) of |
111 val (th, tac) = case (prop_of pre_thm) of |
112 Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
112 Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
113 let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1)) |
113 let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1)) |
114 in |
114 in |
115 ((pth RS iffD2) RS pre_thm, |
115 ((pth RS iffD2) RS pre_thm, |
116 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
116 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
117 end |
117 end |
118 | _ => (pre_thm, assm_tac i) |
118 | _ => (pre_thm, assm_tac i) |