# HG changeset patch # User wenzelm # Date 1684577081 -7200 # Node ID 40db83793cea92d5df9bec488c701549e1033b4c # Parent b0bcba8afdd8ffc94ef80c229c012618238bb9cf more operations; diff -r b0bcba8afdd8 -r 40db83793cea src/Pure/morphism.ML --- a/src/Pure/morphism.ML Fri May 19 22:09:06 2023 +0200 +++ b/src/Pure/morphism.ML Sat May 20 12:04:41 2023 +0200 @@ -56,7 +56,9 @@ val typ_morphism: string -> (typ -> typ) -> morphism val term_morphism': string -> (theory -> term -> term) -> morphism val term_morphism: string -> (term -> term) -> morphism + val fact_morphism': string -> (theory -> thm list -> thm list) -> morphism val fact_morphism: string -> (thm list -> thm list) -> morphism + val thm_morphism': string -> (theory -> thm -> thm) -> morphism val thm_morphism: string -> (thm -> thm) -> morphism val transfer_morphism: theory -> morphism val transfer_morphism': Proof.context -> morphism @@ -202,7 +204,9 @@ fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []}; fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []}; fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []}; +fun fact_morphism' a fact = morphism a {binding = [], typ = [], term = [], fact = [fact o the_theory]}; fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]}; +fun thm_morphism' a thm = morphism a {binding = [], typ = [], term = [], fact = [map o thm o the_theory]}; fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]}; fun transfer_morphism thy = fact_morphism "transfer" I |> set_context thy;