# HG changeset patch
# User haftmann
# Date 1196236897 -3600
# Node ID 4ed49eccb1eb806a290c5933a4f8ee61266b2678
# Parent  aa16cd919dccc5c9f7080296201ec205531d90ed
dropped implicit assumption proof

diff -r aa16cd919dcc -r 4ed49eccb1eb src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:37 2007 +0100
@@ -288,7 +288,7 @@
    apply (rule commute [THEN trans])
      apply (rule_tac [3] commute [THEN trans, symmetric])
        apply (rule_tac [5] sym)
-       apply (assumption | rule congt |
+       apply (rule congt | assumption |
          erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
   done
 
diff -r aa16cd919dcc -r 4ed49eccb1eb src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Lattices.thy	Wed Nov 28 09:01:37 2007 +0100
@@ -39,7 +39,8 @@
   assumes "a \<sqsubseteq> x"
   shows "a \<sqinter> b \<sqsubseteq> x"
 proof (rule order_trans)
-  show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
+  from assms show "a \<sqsubseteq> x" .
+  show "a \<sqinter> b \<sqsubseteq> a" by simp 
 qed
 lemmas (in -) [rule del] = le_infI1
 
@@ -47,7 +48,8 @@
   assumes "b \<sqsubseteq> x"
   shows "a \<sqinter> b \<sqsubseteq> x"
 proof (rule order_trans)
-  show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
+  from assms show "b \<sqsubseteq> x" .
+  show "a \<sqinter> b \<sqsubseteq> b" by simp
 qed
 lemmas (in -) [rule del] = le_infI2
 
diff -r aa16cd919dcc -r 4ed49eccb1eb src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Nov 28 09:01:34 2007 +0100
+++ b/src/HOL/Nat.thy	Wed Nov 28 09:01:37 2007 +0100
@@ -813,20 +813,20 @@
 \item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
 \end{itemize}
 NB: the proof also shows how to use the previous lemma. *}
-corollary infinite_descent0_measure[case_names 0 smaller]:
-assumes 0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
-and     1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
-shows "P x"
+corollary infinite_descent0_measure [case_names 0 smaller]:
+  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
+    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
+  shows "P x"
 proof -
   obtain n where "n = V x" by auto
-  moreover have "!!x. V x = n \<Longrightarrow> P x"
+  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
   proof (induct n rule: infinite_descent0)
     case 0 -- "i.e. $V(x) = 0$"
-    with 0 show "P x" by auto
+    with A0 show "P x" by auto
   next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
     case (smaller n)
     then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
-    with 1 obtain y where "V y < V x \<and> \<not> P y" by auto
+    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
     with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
     thus ?case by auto
   qed