# HG changeset patch
# User Andreas Lochbihler
# Date 1423659132 -3600
# Node ID 28e1349eb48b05fff9f258657c990fe8d2b37f37
# Parent  509caf5edfa6795378da9b855a2847d5843a91eb
add parametricity rule for Ex1

diff -r 509caf5edfa6 -r 28e1349eb48b src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Feb 11 13:51:16 2015 +0100
+++ b/src/HOL/Transfer.thy	Wed Feb 11 13:52:12 2015 +0100
@@ -460,6 +460,11 @@
   shows "((A ===> op =) ===> op =) Ex Ex"
   using assms unfolding bi_total_def rel_fun_def by fast
 
+lemma Ex1_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A" "bi_total A"
+  shows "((A ===> op =) ===> op =) Ex1 Ex1"
+unfolding Ex1_def[abs_def] by transfer_prover
+
 declare If_transfer [transfer_rule]
 
 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"