src/HOL/Tools/Nitpick/nitpick_isar.ML
changeset 41856 7244589c8ccc
parent 41803 ef13e3b7cbaf
child 41875 e3cd0dce9b1a
equal deleted inserted replaced
41855:c3b6e69da386 41856:7244589c8ccc
    56    ("merge_type_vars", "false"),
    56    ("merge_type_vars", "false"),
    57    ("binary_ints", "smart"),
    57    ("binary_ints", "smart"),
    58    ("destroy_constrs", "true"),
    58    ("destroy_constrs", "true"),
    59    ("specialize", "true"),
    59    ("specialize", "true"),
    60    ("star_linear_preds", "true"),
    60    ("star_linear_preds", "true"),
       
    61    ("total_consts", "smart"),
    61    ("preconstr", "smart"),
    62    ("preconstr", "smart"),
    62    ("peephole_optim", "true"),
    63    ("peephole_optim", "true"),
    63    ("datatype_sym_break", "5"),
    64    ("datatype_sym_break", "5"),
    64    ("kodkod_sym_break", "15"),
    65    ("kodkod_sym_break", "15"),
    65    ("timeout", "30"),
    66    ("timeout", "30"),
    89    ("dont_merge_type_vars", "merge_type_vars"),
    90    ("dont_merge_type_vars", "merge_type_vars"),
    90    ("unary_ints", "binary_ints"),
    91    ("unary_ints", "binary_ints"),
    91    ("dont_destroy_constrs", "destroy_constrs"),
    92    ("dont_destroy_constrs", "destroy_constrs"),
    92    ("dont_specialize", "specialize"),
    93    ("dont_specialize", "specialize"),
    93    ("dont_star_linear_preds", "star_linear_preds"),
    94    ("dont_star_linear_preds", "star_linear_preds"),
       
    95    ("partial_consts", "total_consts"),
    94    ("dont_preconstr", "preconstr"),
    96    ("dont_preconstr", "preconstr"),
    95    ("no_peephole_optim", "peephole_optim"),
    97    ("no_peephole_optim", "peephole_optim"),
    96    ("no_debug", "debug"),
    98    ("no_debug", "debug"),
    97    ("quiet", "verbose"),
    99    ("quiet", "verbose"),
    98    ("no_overlord", "overlord"),
   100    ("no_overlord", "overlord"),
   251     val merge_type_vars = lookup_bool "merge_type_vars"
   253     val merge_type_vars = lookup_bool "merge_type_vars"
   252     val binary_ints = lookup_bool_option "binary_ints"
   254     val binary_ints = lookup_bool_option "binary_ints"
   253     val destroy_constrs = lookup_bool "destroy_constrs"
   255     val destroy_constrs = lookup_bool "destroy_constrs"
   254     val specialize = lookup_bool "specialize"
   256     val specialize = lookup_bool "specialize"
   255     val star_linear_preds = lookup_bool "star_linear_preds"
   257     val star_linear_preds = lookup_bool "star_linear_preds"
       
   258     val total_consts = lookup_bool_option "total_consts"
   256     val preconstrs =
   259     val preconstrs =
   257       lookup_bool_option_assigns read_term_polymorphic "preconstr"
   260       lookup_bool_option_assigns read_term_polymorphic "preconstr"
   258     val peephole_optim = lookup_bool "peephole_optim"
   261     val peephole_optim = lookup_bool "peephole_optim"
   259     val datatype_sym_break = lookup_int "datatype_sym_break"
   262     val datatype_sym_break = lookup_int "datatype_sym_break"
   260     val kodkod_sym_break = lookup_int "kodkod_sym_break"
   263     val kodkod_sym_break = lookup_int "kodkod_sym_break"
   283      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
   286      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
   284      debug = debug, verbose = verbose, overlord = overlord,
   287      debug = debug, verbose = verbose, overlord = overlord,
   285      user_axioms = user_axioms, assms = assms, whacks = whacks,
   288      user_axioms = user_axioms, assms = assms, whacks = whacks,
   286      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
   289      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
   287      destroy_constrs = destroy_constrs, specialize = specialize,
   290      destroy_constrs = destroy_constrs, specialize = specialize,
   288      star_linear_preds = star_linear_preds, preconstrs = preconstrs,
   291      star_linear_preds = star_linear_preds, total_consts = total_consts,
   289      peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
   292      preconstrs = preconstrs, peephole_optim = peephole_optim,
       
   293      datatype_sym_break = datatype_sym_break,
   290      kodkod_sym_break = kodkod_sym_break, timeout = timeout,
   294      kodkod_sym_break = kodkod_sym_break, timeout = timeout,
   291      tac_timeout = tac_timeout, max_threads = max_threads,
   295      tac_timeout = tac_timeout, max_threads = max_threads,
   292      show_datatypes = show_datatypes, show_consts = show_consts,
   296      show_datatypes = show_datatypes, show_consts = show_consts,
   293      evals = evals, formats = formats, atomss = atomss,
   297      evals = evals, formats = formats, atomss = atomss,
   294      max_potential = max_potential, max_genuine = max_genuine,
   298      max_potential = max_potential, max_genuine = max_genuine,