equal
deleted
inserted
replaced
166 | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) |
166 | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) |
167 in |
167 in |
168 mk_split_lambda' xs t |
168 mk_split_lambda' xs t |
169 end; |
169 end; |
170 |
170 |
171 fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B |
171 fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B |
172 | strip_imp_prems _ = []; |
172 | strip_imp_prems _ = []; |
173 |
173 |
174 fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B |
174 fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B |
175 | strip_imp_concl A = A : term; |
175 | strip_imp_concl A = A : term; |
176 |
176 |
177 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
177 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
178 |
178 |
179 fun cpu_time description f = |
179 fun cpu_time description f = |