# HG changeset patch
# User Andreas Lochbihler
# Date 1411046603 -7200
# Node ID 09a2c3e08ec21ec5a0e685bca533816072f7f833
# Parent  8af1e68d7e1aeff089af6e0b4bd7f2250c411369
add lemma

diff -r 8af1e68d7e1a -r 09a2c3e08ec2 src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 00:03:46 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 15:23:23 2014 +0200
@@ -36,4 +36,8 @@
   in [(@{const_syntax phantom}, phantom_tr')] end
 *}
 
+lemma of_phantom_inject [simp]:
+  "of_phantom x = of_phantom y \<longleftrightarrow> x = y"
+by(cases x y rule: phantom.exhaust[case_product phantom.exhaust]) simp
+
 end