# HG changeset patch
# User wenzelm
# Date 1184671157 -7200
# Node ID bfb3b1e1d766670033828b6591dc72fcba6e5e0f
# Parent  2acd9d79d855c9fd8b592440a410d728656ea99d
tuned specifications;

diff -r 2acd9d79d855 -r bfb3b1e1d766 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Jul 16 21:39:56 2007 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Tue Jul 17 13:19:17 2007 +0200
@@ -33,26 +33,26 @@
 judgment
   Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
 
-consts
-  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25)
+axiomatization
+  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
   All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
-
-axioms
-  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
-  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+where
+  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
+  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
+  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
   allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
 
 
 subsubsection {* Extensional equality *}
 
-consts
+axiomatization
   equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
+where
+  refl [intro]: "x = x" and
+  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
 
-axioms
-  refl [intro]: "x = x"
-  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
-  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
+axiomatization where
+  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
   iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
 
 theorem sym [sym]: "x = y \<Longrightarrow> y = x"
@@ -101,7 +101,7 @@
 
 definition
   Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
-  "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+  "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
 
 abbreviation
   not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50) where