# HG changeset patch
# User wenzelm
# Date 1452595775 -3600
# Node ID dc4c9748a86eb98f66923231764f21f6d782af90
# Parent  33ce5f41a9e1accb6b9ddaca93cfe71af76a9d9b
eliminated old defs;

diff -r 33ce5f41a9e1 -r dc4c9748a86e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jan 12 11:48:43 2016 +0100
+++ b/src/HOL/HOL.thy	Tue Jan 12 11:49:35 2016 +0100
@@ -69,25 +69,38 @@
 
 typedecl bool
 
-judgment
-  Trueprop      :: "bool \<Rightarrow> prop"                   ("(_)" 5)
+judgment Trueprop :: "bool \<Rightarrow> prop"  ("(_)" 5)
+
+axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
+  and eq :: "['a, 'a] \<Rightarrow> bool"  (infixl "=" 50)
+  and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+
 
-axiomatization
-  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<longrightarrow>" 25)  and
-  eq            :: "['a, 'a] \<Rightarrow> bool"               (infixl "=" 50)  and
-  The           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+subsubsection \<open>Defined connectives and quantifiers\<close>
+
+definition True :: bool
+  where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
+
+definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10)
+  where "All P \<equiv> (P = (\<lambda>x. True))"
 
-consts
-  True          :: bool
-  False         :: bool
-  Not           :: "bool \<Rightarrow> bool"                   ("\<not> _" [40] 40)
+definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10)
+  where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
+
+definition False :: bool
+  where "False \<equiv> (\<forall>P. P)"
+
+definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40)
+  where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
-  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<and>" 35)
-  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<or>" 30)
+definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35)
+  where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
 
-  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<forall>" 10)
-  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>" 10)
-  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>!" 10)
+definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
+  where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
+
+definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>!" 10)
+  where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
@@ -167,16 +180,6 @@
   iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
   True_or_False: "(P = True) \<or> (P = False)"
 
-defs
-  True_def:     "True      \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
-  All_def:      "All P     \<equiv> (P = (\<lambda>x. True))"
-  Ex_def:       "Ex P      \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
-  False_def:    "False     \<equiv> (\<forall>P. P)"
-  not_def:      "\<not> P       \<equiv> P \<longrightarrow> False"
-  and_def:      "P \<and> Q     \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
-  or_def:       "P \<or> Q     \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
-  Ex1_def:      "Ex1 P     \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
-
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
   where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"