# HG changeset patch
# User Andreas Lochbihler
# Date 1411107963 -7200
# Node ID 00aaaa7bd7526c784fa0bb9dc7ff846c323e2765
# Parent  2ee61d28c667de432c9aa0655112d96db9ca3f03# Parent  09a2c3e08ec21ec5a0e685bca533816072f7f833
merged

diff -r 2ee61d28c667 -r 00aaaa7bd752 src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 19:01:50 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Fri Sep 19 08:26:03 2014 +0200
@@ -30,4 +30,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