src/HOL/Import/HOL4Compat.thy
changeset 17188 a26a4fc323ed
parent 16417 9bc16273c2d4
child 19064 bf19cc5a7899
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Aug 29 16:25:24 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Aug 29 16:51:39 2005 +0200
     1.3 @@ -26,6 +26,9 @@
     1.4  lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
     1.5    by safe
     1.6  
     1.7 +(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
     1.8 +  by simp*)
     1.9 +
    1.10  consts
    1.11    ISL :: "'a + 'b => bool"
    1.12    ISR :: "'a + 'b => bool"