equal
deleted
inserted
replaced
513 |
513 |
514 fun gen_assume f exp args state = |
514 fun gen_assume f exp args state = |
515 state |
515 state |
516 |> assert_forward |
516 |> assert_forward |
517 |> map_context_result (f exp args) |
517 |> map_context_result (f exp args) |
518 |> (fn (st, (factss, prems)) => |
518 |> these_factss; |
519 these_factss (st, factss) |
|
520 |> put_thms ("prems", prems)); |
|
521 |
519 |
522 val assm = gen_assume ProofContext.assume; |
520 val assm = gen_assume ProofContext.assume; |
523 val assm_i = gen_assume ProofContext.assume_i; |
521 val assm_i = gen_assume ProofContext.assume_i; |
524 val assume = assm ProofContext.export_assume; |
522 val assume = assm ProofContext.export_assume; |
525 val assume_i = assm_i ProofContext.export_assume; |
523 val assume_i = assm_i ProofContext.export_assume; |