src/Pure/Isar/proof_context.ML
changeset 24812 8c2e8cf22fad
parent 24778 3e7f71caae18
child 24922 577ec55380d8
equal deleted inserted replaced
24811:3bf788a0c49a 24812:8c2e8cf22fad
     8 *)
     8 *)
     9 
     9 
    10 signature PROOF_CONTEXT =
    10 signature PROOF_CONTEXT =
    11 sig
    11 sig
    12   val theory_of: Proof.context -> theory
    12   val theory_of: Proof.context -> theory
       
    13   val tsig_of: Proof.context -> Type.tsig
    13   val init: theory -> Proof.context
    14   val init: theory -> Proof.context
    14   type mode
    15   type mode
    15   val mode_default: mode
    16   val mode_default: mode
    16   val mode_stmt: mode
    17   val mode_stmt: mode
    17   val mode_pattern: mode
    18   val mode_pattern: mode