Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added theorems_of;
authorwenzelm
Mon, 26 Feb 2007 20:14:52 +0100
changeset 22358 4d8a9e3a29f8
parent 22357 914b5a0b61be
child 22359 94a794672c8b
added theorems_of;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle