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.
tuned signature;
authorwenzelm
Thu, 09 Jun 2016 12:21:15 +0200
changeset 63269 27d51aa2d711
parent 63268 df955dd2dc09
child 63270 7dd3ee7ee422
tuned signature;
src/Pure/Isar/generic_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/generic_target.ML	Thu Jun 09 12:16:52 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Jun 09 12:21:15 2016 +0200
@@ -20,6 +20,12 @@
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
 
   (*nested local theories primitives*)
+  val standard_facts: local_theory -> Proof.context ->
+    (Attrib.binding * Attrib.thms) list -> (Attrib.binding * Attrib.thms) list
+  val standard_notes: (int * int -> bool) -> string -> (Attrib.binding * Attrib.thms) list ->
+    local_theory -> local_theory
+  val standard_declaration: (int * int -> bool) ->
+    (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
isabelle