Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL4Compat.thy
changeset 17188 a26a4fc323ed
parent 16417 9bc16273c2d4
child 19064 bf19cc5a7899 
--- a/src/HOL/Import/HOL4Compat.thy	Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Aug 29 16:51:39 2005 +0200
@@ -26,6 +26,9 @@
 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
   by safe
 
+(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
+  by simp*)
+
 consts
   ISL :: "'a + 'b => bool"
   ISR :: "'a + 'b => bool"
isabelle