Lines Matching defs:proof
307 type state = {env : subst, depth : int, proof : thm list, offset : int};
309 fun update_env f ({env, depth, proof, offset} : state) =
310 {env = f env, depth = depth, proof = proof, offset = offset};
312 fun update_depth f ({env, depth, proof, offset} : state) =
313 {env = env, depth = f depth, proof = proof, offset = offset};
315 fun update_proof f ({env, depth, proof, offset} : state) =
316 {env = env, depth = depth, proof = f proof, offset = offset};
318 fun update_offset f ({env, depth, proof, offset} : state) =
319 {env = env, depth = depth, proof = proof, offset = f offset};
379 fun grab_unit units (s as {proof = th :: _, ...} : state) =
387 | grab_unit _ {proof = [], ...} = raise Bug "grab_unit: no thms";
490 and expand_rule ancestors g cont {env, depth, proof, offset} r () =
503 {env = env, depth = depth, proof = proof, offset = offset}
527 fun meson_finally g ({env, proof, ...} : state) =
529 val () = assert (length proof = length g) (Bug "meson: bad final state")
531 val proof' = map (INST env) (rev proof)
533 (foldl (fn (h,t)=>t^" "^thm_to_string h^"\n") "meson_finally:\n" proof')
535 assert (List.all (uncurry thm_proves) (zip proof' g'))
538 (SOME (FRESH_VARSL proof'), CHOICE no_choice)
545 {env = |<>|, depth = depth, proof = [], offset = 0});