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
Mon, 31 Aug 2015 19:04:01 +0200
changeset 61064 01b23bfb4947
parent 61063 d0c21a68d9c6
child 61065 ca4ebc63d8ac
tuned signature;
src/Pure/morphism.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/morphism.ML	Mon Aug 31 19:02:00 2015 +0200
+++ b/src/Pure/morphism.ML	Mon Aug 31 19:04:01 2015 +0200
@@ -35,6 +35,7 @@
   val fact_morphism: string -> (thm list -> thm list) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
+  val trim_context_morphism: morphism
   val identity: morphism
   val compose: morphism -> morphism -> morphism
   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
@@ -91,6 +92,7 @@
 fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
 val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
+val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
 val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
isabelle