equal
deleted
inserted
replaced
244 pretties_for_formulas ctxt ("Nitpicking " ^ |
244 pretties_for_formulas ctxt ("Nitpicking " ^ |
245 (if i <> 1 orelse n <> 1 then |
245 (if i <> 1 orelse n <> 1 then |
246 "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n |
246 "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n |
247 else |
247 else |
248 "goal")) [Logic.list_implies (assm_ts, orig_t)])) |
248 "goal")) [Logic.list_implies (assm_ts, orig_t)])) |
|
249 val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" |
|
250 o Date.fromTimeLocal o Time.now) |
249 val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) |
251 val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) |
250 else orig_t |
252 else orig_t |
251 val tfree_table = |
253 val tfree_table = |
252 if merge_type_vars then |
254 if merge_type_vars then |
253 merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals) |
255 merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals) |