Lines Matching defs:facts
156 {facts : factdb, subtypes : vthm ovdiscrim};
193 PSUBTYPE_CONTEXT {facts = set_factdb, subtypes = empty_ovdiscrim};
196 val psubtype_context_facts = #facts o dest_psubtype_context;
198 fun psubtype_context_update_facts f (PSUBTYPE_CONTEXT {facts, subtypes}) =
199 PSUBTYPE_CONTEXT {facts = f facts, subtypes = subtypes};
200 fun psubtype_context_update_subtypes f (PSUBTYPE_CONTEXT {facts, subtypes}) =
201 PSUBTYPE_CONTEXT {facts = facts, subtypes = f subtypes};
229 add_string "{#facts =",
231 pp_int (factdb_size (#facts c)),
315 fun cached_basic_subtypes facts tm =
317 basic_subtypes facts tm
320 ((tm, depth), fn () => basic_subtypes facts tm)
321 and basic_subtypes facts tm =
329 val cond_provers = map (cond_prover facts) conds
339 and cond_prover facts cond =
350 val facts' = factdb_add_vthm (empty_vars, ASSUME asm) facts
351 val basics = cached_basic_subtypes facts' elt'
352 val facts'' = factdb_add_vthms basics facts'
363 val pre_results = set_prove_depth facts'' depth (before_vars, goal)
409 val facts = factdb_add_vthms subtypes (subtype_context_facts sc)
410 val res = set_prove_depth facts depth (vars, goal)