equal
deleted
inserted
replaced
48 val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition |
48 val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition |
49 val theory_to_proof: (theory -> ProofHistory.T) -> transition -> transition |
49 val theory_to_proof: (theory -> ProofHistory.T) -> transition -> transition |
50 val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition |
50 val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition |
51 type isar |
51 type isar |
52 val trace: bool ref |
52 val trace: bool ref |
|
53 val exn_message: exn -> string |
53 val apply: bool -> transition -> state -> (state * (exn * string) option) option |
54 val apply: bool -> transition -> state -> (state * (exn * string) option) option |
54 val excursion: transition list -> unit |
55 val excursion: transition list -> unit |
55 val set_state: state -> unit |
56 val set_state: state -> unit |
56 val get_state: unit -> state |
57 val get_state: unit -> state |
57 val exn: unit -> (exn * string) option |
58 val exn: unit -> (exn * string) option |