src/HOL/ex/Higher_Order_Logic.thy
changeset 19380 b808efaa5828
parent 16417 9bc16273c2d4
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -93,10 +93,9 @@
     1.4    Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<exists>" 10)
     1.5    "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
     1.6  
     1.7 -syntax
     1.8 -  "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
     1.9 -translations
    1.10 -  "x \<noteq> y"  \<rightleftharpoons>  "\<not> (x = y)"
    1.11 +abbreviation
    1.12 +  not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
    1.13 +  "x \<noteq> y \<equiv> \<not> (x = y)"
    1.14  
    1.15  theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
    1.16  proof (unfold false_def)