18 val defs = Nitpick_HOL.all_axioms_of @{context} subst |> #1 |
18 val defs = Nitpick_HOL.all_axioms_of @{context} subst |> #1 |
19 val def_table = Nitpick_HOL.const_def_table @{context} subst defs |
19 val def_table = Nitpick_HOL.const_def_table @{context} subst defs |
20 val hol_ctxt : Nitpick_HOL.hol_context = |
20 val hol_ctxt : Nitpick_HOL.hol_context = |
21 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], |
21 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], |
22 stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, |
22 stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, |
23 binary_ints = SOME false, destroy_constrs = false, specialize = false, |
23 whacks = [], binary_ints = SOME false, destroy_constrs = false, |
24 star_linear_preds = false, fast_descrs = false, tac_timeout = NONE, |
24 specialize = false, star_linear_preds = false, fast_descrs = false, |
25 evals = [], case_names = [], def_table = def_table, |
25 tac_timeout = NONE, evals = [], case_names = [], def_table = def_table, |
26 nondef_table = Symtab.empty, user_nondefs = [], |
26 nondef_table = Symtab.empty, user_nondefs = [], |
27 simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, |
27 simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, |
28 choice_spec_table = Symtab.empty, intro_table = Symtab.empty, |
28 choice_spec_table = Symtab.empty, intro_table = Symtab.empty, |
29 ground_thm_table = Inttab.empty, ersatz_table = [], |
29 ground_thm_table = Inttab.empty, ersatz_table = [], |
30 skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], |
30 skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], |