equal
deleted
inserted
replaced
12 begin |
12 begin |
13 |
13 |
14 ML {* |
14 ML {* |
15 exception FAIL |
15 exception FAIL |
16 |
16 |
17 val defs = NitpickHOL.all_axioms_of @{theory} |> #1 |
17 val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1 |
18 val def_table = NitpickHOL.const_def_table @{context} defs |
18 val def_table = Nitpick_HOL.const_def_table @{context} defs |
19 val ext_ctxt = |
19 val ext_ctxt = |
20 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], |
20 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], |
21 user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false, |
21 user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false, |
22 specialize = false, skolemize = false, star_linear_preds = false, |
22 specialize = false, skolemize = false, star_linear_preds = false, |
23 uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [], |
23 uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [], |