# HG changeset patch
# User wenzelm
# Date 1211123003 -7200
# Node ID ed3a58a9eae132b71f8dc7ec15fc6b73473c36c4
# Parent  e3f04fdd994d358929cd24db212bf26c58a02998
converted to regular application syntax;

diff -r e3f04fdd994d -r ed3a58a9eae1 src/FOL/ex/First_Order_Logic.thy
--- a/src/FOL/ex/First_Order_Logic.thy	Sun May 18 17:03:20 2008 +0200
+++ b/src/FOL/ex/First_Order_Logic.thy	Sun May 18 17:03:23 2008 +0200
@@ -110,7 +110,7 @@
   equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
 where
   refl [intro]: "x = x" and
-  subst: "x = y \<Longrightarrow> P(x) \<Longrightarrow> P(y)"
+  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
 
 theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
   by (rule subst)
@@ -128,32 +128,32 @@
   All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) and
   Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
 where
-  allI [intro]: "(\<And>x. P(x)) \<Longrightarrow> \<forall>x. P(x)" and
-  allD [dest]: "\<forall>x. P(x) \<Longrightarrow> P(a)" and
-  exI [intro]: "P(a) \<Longrightarrow> \<exists>x. P(x)" and
-  exE [elim]: "\<exists>x. P(x) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> C) \<Longrightarrow> C"
+  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
+  allD [dest]: "\<forall>x. P x \<Longrightarrow> P a" and
+  exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" and
+  exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
 
 
-lemma "(\<exists>x. P(f(x))) \<longrightarrow> (\<exists>y. P(y))"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
-  assume "\<exists>x. P(f(x))"
-  then show "\<exists>y. P(y)"
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
   proof
-    fix x assume "P(f(x))"
+    fix x assume "P (f x)"
     then show ?thesis ..
   qed
 qed
 
-lemma "(\<exists>x. \<forall>y. R(x, y)) \<longrightarrow> (\<forall>y. \<exists>x. R(x, y))"
+lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
 proof
-  assume "\<exists>x. \<forall>y. R(x, y)"
-  then show "\<forall>y. \<exists>x. R(x, y)"
+  assume "\<exists>x. \<forall>y. R x y"
+  then show "\<forall>y. \<exists>x. R x y"
   proof
-    fix x assume a: "\<forall>y. R(x, y)"
+    fix x assume a: "\<forall>y. R x y"
     show ?thesis
     proof
-      fix y from a have "R(x, y)" ..
-      then show "\<exists>x. R(x, y)" ..
+      fix y from a have "R x y" ..
+      then show "\<exists>x. R x y" ..
     qed
   qed
 qed
diff -r e3f04fdd994d -r ed3a58a9eae1 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun May 18 17:03:20 2008 +0200
+++ b/src/Pure/Pure.thy	Sun May 18 17:03:23 2008 +0200
@@ -14,14 +14,14 @@
 lemmas meta_impE = meta_mp [elim_format]
 
 lemma meta_spec:
-  assumes "!!x. PROP P(x)"
-  shows "PROP P(x)"
-    by (rule `!!x. PROP P(x)`)
+  assumes "!!x. PROP P x"
+  shows "PROP P x"
+    by (rule `!!x. PROP P x`)
 
 lemmas meta_allE = meta_spec [elim_format]
 
 lemma swap_params:
-  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
+  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
 
 
 subsection {* Embedded terms *}
@@ -39,22 +39,22 @@
 
 lemma all_conjunction:
   includes meta_conjunction_syntax
-  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
+  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
 proof
-  assume conj: "!!x. PROP A(x) && PROP B(x)"
-  show "(!!x. PROP A(x)) && (!!x. PROP B(x))"
+  assume conj: "!!x. PROP A x && PROP B x"
+  show "(!!x. PROP A x) && (!!x. PROP B x)"
   proof -
     fix x
-    from conj show "PROP A(x)" by (rule conjunctionD1)
-    from conj show "PROP B(x)" by (rule conjunctionD2)
+    from conj show "PROP A x" by (rule conjunctionD1)
+    from conj show "PROP B x" by (rule conjunctionD2)
   qed
 next
-  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
+  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
   fix x
-  show "PROP A(x) && PROP B(x)"
+  show "PROP A x && PROP B x"
   proof -
-    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
-    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
+    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
+    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   qed
 qed