src/Pure/Isar/proof_context.ML
changeset 56864 0446c7ac2e32
parent 56438 7f6b2634d853
child 56867 224109105008
equal deleted inserted replaced
56863:5fdb61a9a010 56864:0446c7ac2e32
   160     (term * term) * Context.generic
   160     (term * term) * Context.generic
   161   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   161   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   162   val print_syntax: Proof.context -> unit
   162   val print_syntax: Proof.context -> unit
   163   val print_abbrevs: Proof.context -> unit
   163   val print_abbrevs: Proof.context -> unit
   164   val print_binds: Proof.context -> unit
   164   val print_binds: Proof.context -> unit
       
   165   val pretty_local_facts: Proof.context -> bool -> Pretty.T list
   165   val print_local_facts: Proof.context -> bool -> unit
   166   val print_local_facts: Proof.context -> bool -> unit
   166   val print_cases: Proof.context -> unit
   167   val print_cases: Proof.context -> unit
   167   val debug: bool Config.T
   168   val debug: bool Config.T
   168   val verbose: bool Config.T
   169   val verbose: bool Config.T
   169   val pretty_ctxt: Proof.context -> Pretty.T list
   170   val pretty_ctxt: Proof.context -> Pretty.T list