# HG changeset patch
# User krauss
# Date 1305876696 -7200
# Node ID 36abaf4cce1f6f95f49a8e3a3964b6afca5d3ef9
# Parent  43b0f61f56d020a8e4115962deeb0b93602326a5
clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton

diff -r 43b0f61f56d0 -r 36abaf4cce1f src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Fri May 20 08:16:56 2011 +0200
+++ b/src/HOL/Nat_Transfer.thy	Fri May 20 09:31:36 2011 +0200
@@ -11,12 +11,10 @@
 subsection {* Generic transfer machinery *}
 
 definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
-  where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
+  where "transfer_morphism f A \<longleftrightarrow> True"
 
-lemma transfer_morphismI:
-  assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
-  shows "transfer_morphism f A"
-  using assms by (auto simp add: transfer_morphism_def)
+lemma transfer_morphismI[intro]: "transfer_morphism f A"
+  by (simp add: transfer_morphism_def)
 
 use "Tools/transfer.ML"
 
@@ -27,8 +25,7 @@
 
 text {* set up transfer direction *}
 
-lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
-  by (rule transfer_morphismI) simp
+lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
 
 declare transfer_morphism_nat_int [transfer add
   mode: manual
@@ -266,8 +263,7 @@
 
 text {* set up transfer direction *}
 
-lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
-by (rule transfer_morphismI) simp
+lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual