src/Pure/Isar/proof.ML
changeset 7011 7e8e9a26ba2c
parent 6996 1a28d968c5aa
child 7176 a329a37ed91a
equal deleted inserted replaced
7010:63120b6dca50 7011:7e8e9a26ba2c
     9 sig
     9 sig
    10   type context
    10   type context
    11   type state
    11   type state
    12   exception STATE of string * state
    12   exception STATE of string * state
    13   val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
    13   val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
       
    14   val init_state: theory -> state
    14   val context_of: state -> context
    15   val context_of: state -> context
    15   val theory_of: state -> theory
    16   val theory_of: state -> theory
    16   val sign_of: state -> Sign.sg
    17   val sign_of: state -> Sign.sg
    17   val the_facts: state -> thm list
    18   val the_facts: state -> thm list
    18   val the_fact: state -> thm
    19   val the_fact: state -> thm
   641 fun end_proof bot state =
   642 fun end_proof bot state =
   642   state
   643   state
   643   |> assert_forward
   644   |> assert_forward
   644   |> close_block
   645   |> close_block
   645   |> assert_bottom bot
   646   |> assert_bottom bot
   646   |> assert_current_goal true;
   647   |> assert_current_goal true
       
   648   |> goal_facts (K []);
   647 
   649 
   648 
   650 
   649 (* local_qed *)
   651 (* local_qed *)
   650 
   652 
   651 fun finish_local (print_result, print_rule) state =
   653 fun finish_local (print_result, print_rule) state =