src/Pure/Isar/proof_context.ML
changeset 36610 bafd82950e24
parent 36542 7cb6b40d19b2
child 37145 01aa36932739
equal deleted inserted replaced
36609:6ed6112f0a95 36610:bafd82950e24
     7 *)
     7 *)
     8 
     8 
     9 signature PROOF_CONTEXT =
     9 signature PROOF_CONTEXT =
    10 sig
    10 sig
    11   val theory_of: Proof.context -> theory
    11   val theory_of: Proof.context -> theory
    12   val init: theory -> Proof.context
    12   val init_global: theory -> Proof.context
    13   type mode
    13   type mode
    14   val mode_default: mode
    14   val mode_default: mode
    15   val mode_stmt: mode
    15   val mode_stmt: mode
    16   val mode_pattern: mode
    16   val mode_pattern: mode
    17   val mode_schematic: mode
    17   val mode_schematic: mode