equal
deleted
inserted
replaced
27 destroy_constrs: bool, |
27 destroy_constrs: bool, |
28 specialize: bool, |
28 specialize: bool, |
29 star_linear_preds: bool, |
29 star_linear_preds: bool, |
30 total_consts: bool option, |
30 total_consts: bool option, |
31 needs: term list option, |
31 needs: term list option, |
32 tac_timeout: Time.time option, |
32 tac_timeout: Time.time, |
33 evals: term list, |
33 evals: term list, |
34 case_names: (string * int) list, |
34 case_names: (string * int) list, |
35 def_tables: const_table * const_table, |
35 def_tables: const_table * const_table, |
36 nondef_table: const_table, |
36 nondef_table: const_table, |
37 nondefs: term list, |
37 nondefs: term list, |
269 destroy_constrs: bool, |
269 destroy_constrs: bool, |
270 specialize: bool, |
270 specialize: bool, |
271 star_linear_preds: bool, |
271 star_linear_preds: bool, |
272 total_consts: bool option, |
272 total_consts: bool option, |
273 needs: term list option, |
273 needs: term list option, |
274 tac_timeout: Time.time option, |
274 tac_timeout: Time.time, |
275 evals: term list, |
275 evals: term list, |
276 case_names: (string * int) list, |
276 case_names: (string * int) list, |
277 def_tables: const_table * const_table, |
277 def_tables: const_table * const_table, |
278 nondef_table: const_table, |
278 nondef_table: const_table, |
279 nondefs: term list, |
279 nondefs: term list, |
2067 can (SINGLE (Classical.safe_tac ctxt) #> the |
2067 can (SINGLE (Classical.safe_tac ctxt) #> the |
2068 #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) |
2068 #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) |
2069 #> the #> Goal.finish ctxt) goal |
2069 #> the #> Goal.finish ctxt) goal |
2070 |
2070 |
2071 val max_cached_wfs = 50 |
2071 val max_cached_wfs = 50 |
2072 val cached_timeout = |
2072 val cached_timeout = Synchronized.var "Nitpick_HOL.cached_timeout" Time.zeroTime |
2073 Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime) |
|
2074 val cached_wf_props = |
2073 val cached_wf_props = |
2075 Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list) |
2074 Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list) |
2076 |
2075 |
2077 val termination_tacs = [Lexicographic_Order.lex_order_tac true, |
2076 val termination_tacs = [Lexicographic_Order.lex_order_tac true, |
2078 ScnpReconstruct.sizechange_tac] |
2077 ScnpReconstruct.sizechange_tac] |