# HG changeset patch
# User wenzelm
# Date 1337780410 -7200
# Node ID b74655182ed6c226400c957ac839f127fe70438d
# Parent  46c73ad5f7c034fa5f5819178a9f681dcb9a501f# Parent  e0a85be4fca0b696874689c142fc522107c514c0
merged

diff -r 46c73ad5f7c0 -r b74655182ed6 Admin/contributed_components
--- a/Admin/contributed_components	Wed May 23 13:37:26 2012 +0200
+++ b/Admin/contributed_components	Wed May 23 15:40:10 2012 +0200
@@ -1,6 +1,6 @@
 #contributed components
 contrib/cvc3-2.2
-contrib_devel/e-1.5
+contrib/e-1.5
 contrib/hol-light-bundle-0.5-126
 contrib/kodkodi-1.2.16
 contrib/spass-3.8ds
diff -r 46c73ad5f7c0 -r b74655182ed6 src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 13:37:26 2012 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 15:40:10 2012 +0200
@@ -17,18 +17,18 @@
 lemma de_Morgan:
   assumes "\<not> (\<forall>x. P x)"
   shows "\<exists>x. \<not> P x"
-  using assms
-proof (rule contrapos_np)
-  assume a: "\<not> (\<exists>x. \<not> P x)"
-  show "\<forall>x. P x"
+proof (rule classical)
+  assume "\<not> (\<exists>x. \<not> P x)"
+  have "\<forall>x. P x"
   proof
     fix x show "P x"
     proof (rule classical)
       assume "\<not> P x"
       then have "\<exists>x. \<not> P x" ..
-      with a show ?thesis by contradiction
+      with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
     qed
   qed
+  with `\<not> (\<forall>x. P x)` show ?thesis ..
 qed
 
 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
diff -r 46c73ad5f7c0 -r b74655182ed6 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Wed May 23 13:37:26 2012 +0200
+++ b/src/HOL/Library/Product_ord.thy	Wed May 23 15:40:10 2012 +0200
@@ -22,30 +22,30 @@
 end
 
 lemma [code]:
-  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
-  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+  "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+  "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
   unfolding prod_le_def prod_less_def by simp_all
 
-instance prod :: (preorder, preorder) preorder proof
-qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
+instance prod :: (preorder, preorder) preorder
+  by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
 
-instance prod :: (order, order) order proof
-qed (auto simp add: prod_le_def)
+instance prod :: (order, order) order
+  by default (auto simp add: prod_le_def)
 
-instance prod :: (linorder, linorder) linorder proof
-qed (auto simp: prod_le_def)
+instance prod :: (linorder, linorder) linorder
+  by default (auto simp: prod_le_def)
 
 instantiation prod :: (linorder, linorder) distrib_lattice
 begin
 
 definition
-  inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+  inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
 
 definition
-  sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
+  sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
 
-instance proof
-qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+instance
+  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
 
 end
 
@@ -55,8 +55,8 @@
 definition
   bot_prod_def: "bot = (bot, bot)"
 
-instance proof
-qed (auto simp add: bot_prod_def prod_le_def)
+instance
+  by default (auto simp add: bot_prod_def prod_le_def)
 
 end
 
@@ -66,8 +66,8 @@
 definition
   top_prod_def: "top = (top, top)"
 
-instance proof
-qed (auto simp add: top_prod_def prod_le_def)
+instance
+  by default (auto simp add: top_prod_def prod_le_def)
 
 end
 
@@ -86,11 +86,29 @@
   proof (induct z)
     case (Pair a b)
     show "P (a, b)"
-      apply (induct a arbitrary: b rule: less_induct)
-      apply (rule less_induct [where 'a='b])
-      apply (rule P)
-      apply (auto simp add: prod_less_eq)
-      done
+    proof (induct a arbitrary: b rule: less_induct)
+      case (less a\<^isub>1) note a\<^isub>1 = this
+      show "P (a\<^isub>1, b)"
+      proof (induct b rule: less_induct)
+        case (less b\<^isub>1) note b\<^isub>1 = this
+        show "P (a\<^isub>1, b\<^isub>1)"
+        proof (rule P)
+          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
+          show "P p"
+          proof (cases "fst p < a\<^isub>1")
+            case True
+            then have "P (fst p, snd p)" by (rule a\<^isub>1)
+            then show ?thesis by simp
+          next
+            case False
+            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
+              by (simp_all add: prod_less_eq)
+            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
+            with 1 show ?thesis by simp
+          qed
+        qed
+      qed
+    qed
   qed
 qed