1.1 --- a/Admin/contributed_components	Wed May 23 13:37:26 2012 +0200
     1.2 +++ b/Admin/contributed_components	Wed May 23 15:40:10 2012 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  #contributed components
     1.5  contrib/cvc3-2.2
     1.6 -contrib_devel/e-1.5
     1.7 +contrib/e-1.5
     1.8  contrib/hol-light-bundle-0.5-126
     1.9  contrib/kodkodi-1.2.16
    1.10  contrib/spass-3.8ds

     2.1 --- a/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 13:37:26 2012 +0200
     2.2 +++ b/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 15:40:10 2012 +0200
     2.3 @@ -17,18 +17,18 @@
     2.4  lemma de_Morgan:
     2.5    assumes "\<not> (\<forall>x. P x)"
     2.6    shows "\<exists>x. \<not> P x"
     2.7 -  using assms
     2.8 -proof (rule contrapos_np)
     2.9 -  assume a: "\<not> (\<exists>x. \<not> P x)"
    2.10 -  show "\<forall>x. P x"
    2.11 +proof (rule classical)
    2.12 +  assume "\<not> (\<exists>x. \<not> P x)"
    2.13 +  have "\<forall>x. P x"
    2.14    proof
    2.15      fix x show "P x"
    2.16      proof (rule classical)
    2.17        assume "\<not> P x"
    2.18        then have "\<exists>x. \<not> P x" ..
    2.19 -      with a show ?thesis by contradiction
    2.20 +      with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
    2.21      qed
    2.22    qed
    2.23 +  with `\<not> (\<forall>x. P x)` show ?thesis ..
    2.24  qed
    2.25  
    2.26  theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"

     3.1 --- a/src/HOL/Library/Product_ord.thy	Wed May 23 13:37:26 2012 +0200
     3.2 +++ b/src/HOL/Library/Product_ord.thy	Wed May 23 15:40:10 2012 +0200
     3.3 @@ -22,30 +22,30 @@
     3.4  end
     3.5  
     3.6  lemma [code]:
     3.7 -  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
     3.8 -  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
     3.9 +  "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
    3.10 +  "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    3.11    unfolding prod_le_def prod_less_def by simp_all
    3.12  
    3.13 -instance prod :: (preorder, preorder) preorder proof
    3.14 -qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
    3.15 +instance prod :: (preorder, preorder) preorder
    3.16 +  by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
    3.17  
    3.18 -instance prod :: (order, order) order proof
    3.19 -qed (auto simp add: prod_le_def)
    3.20 +instance prod :: (order, order) order
    3.21 +  by default (auto simp add: prod_le_def)
    3.22  
    3.23 -instance prod :: (linorder, linorder) linorder proof
    3.24 -qed (auto simp: prod_le_def)
    3.25 +instance prod :: (linorder, linorder) linorder
    3.26 +  by default (auto simp: prod_le_def)
    3.27  
    3.28  instantiation prod :: (linorder, linorder) distrib_lattice
    3.29  begin
    3.30  
    3.31  definition
    3.32 -  inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    3.33 +  inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    3.34  
    3.35  definition
    3.36 -  sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    3.37 +  sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    3.38  
    3.39 -instance proof
    3.40 -qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    3.41 +instance
    3.42 +  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    3.43  
    3.44  end
    3.45  
    3.46 @@ -55,8 +55,8 @@
    3.47  definition
    3.48    bot_prod_def: "bot = (bot, bot)"
    3.49  
    3.50 -instance proof
    3.51 -qed (auto simp add: bot_prod_def prod_le_def)
    3.52 +instance
    3.53 +  by default (auto simp add: bot_prod_def prod_le_def)
    3.54  
    3.55  end
    3.56  
    3.57 @@ -66,8 +66,8 @@
    3.58  definition
    3.59    top_prod_def: "top = (top, top)"
    3.60  
    3.61 -instance proof
    3.62 -qed (auto simp add: top_prod_def prod_le_def)
    3.63 +instance
    3.64 +  by default (auto simp add: top_prod_def prod_le_def)
    3.65  
    3.66  end
    3.67  
    3.68 @@ -86,11 +86,29 @@
    3.69    proof (induct z)
    3.70      case (Pair a b)
    3.71      show "P (a, b)"
    3.72 -      apply (induct a arbitrary: b rule: less_induct)
    3.73 -      apply (rule less_induct [where 'a='b])
    3.74 -      apply (rule P)
    3.75 -      apply (auto simp add: prod_less_eq)
    3.76 -      done
    3.77 +    proof (induct a arbitrary: b rule: less_induct)
    3.78 +      case (less a\<^isub>1) note a\<^isub>1 = this
    3.79 +      show "P (a\<^isub>1, b)"
    3.80 +      proof (induct b rule: less_induct)
    3.81 +        case (less b\<^isub>1) note b\<^isub>1 = this
    3.82 +        show "P (a\<^isub>1, b\<^isub>1)"
    3.83 +        proof (rule P)
    3.84 +          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
    3.85 +          show "P p"
    3.86 +          proof (cases "fst p < a\<^isub>1")
    3.87 +            case True
    3.88 +            then have "P (fst p, snd p)" by (rule a\<^isub>1)
    3.89 +            then show ?thesis by simp
    3.90 +          next
    3.91 +            case False
    3.92 +            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
    3.93 +              by (simp_all add: prod_less_eq)
    3.94 +            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
    3.95 +            with 1 show ?thesis by simp
    3.96 +          qed
    3.97 +        qed
    3.98 +      qed
    3.99 +    qed
   3.100    qed
   3.101  qed
   3.102