# HG changeset patch # User wenzelm # Date 1172517292 -3600 # Node ID 4d8a9e3a29f89b3cec0137fd2ec9b39fc278ab61 # Parent 914b5a0b61be29f270c542f572d265cf90df0f41 added theorems_of; diff -r 914b5a0b61be -r 4d8a9e3a29f8 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Feb 26 20:14:47 2007 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Feb 26 20:14:52 2007 +0100 @@ -20,6 +20,7 @@ val const_syntax_name: Proof.context -> string -> string val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context + val theorems_of: Proof.context -> thm list NameSpace.table val fact_index_of: Proof.context -> FactIndex.T val transfer: theory -> Proof.context -> Proof.context val theory: (theory -> theory) -> Proof.context -> Proof.context @@ -250,6 +251,7 @@ val const_syntax_name = Consts.syntax_name o consts_of; val thms_of = #thms o rep_context; +val theorems_of = #1 o thms_of; val fact_index_of = #2 o thms_of; val cases_of = #cases o rep_context;