# HG changeset patch
# User haftmann
# Date 1173426355 -3600
# Node ID 8a54121216871f08174d26b1d7437e52912d2e03
# Parent  c1836b14c63abd95de565e7687d56da004e0610c
*** empty log message ***

diff -r c1836b14c63a -r 8a5412121687 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -323,7 +323,7 @@
 apply (induct_tac "msg")
 apply (simp_all (no_asm_simp) add: exI parts_insert2)
  txt{*MPair case: blast works out the necessary sum itself!*}
- prefer 2 apply (blast elim!: add_leE)
+ prefer 2 apply auto apply (blast elim!: add_leE)
 txt{*Nonce case*}
 apply (rule_tac x = "N + Suc nat" in exI, auto) 
 done
diff -r c1836b14c63a -r 8a5412121687 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Bali/WellForm.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -1634,8 +1634,7 @@
 	by (auto dest!: stat_overrides_commonD)
       from super old wf accmodi_old
       have accmodi_super_method: "Protected \<le> accmodi super_method"
-	by (auto dest!: wf_prog_stat_overridesD
-                 intro: order_trans)
+	by (auto dest!: wf_prog_stat_overridesD)
       from super accmodi_old wf
       have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
 	by (auto dest!: wf_prog_stat_overridesD
@@ -1747,8 +1746,7 @@
     then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
     with Overriding not_static_old accmodi_old wf 
     show ?thesis 
-      by (auto dest!: wf_prog_stat_overridesD
-               intro: order_trans)
+      by (auto dest!: wf_prog_stat_overridesD)
   qed
 qed
  	      
diff -r c1836b14c63a -r 8a5412121687 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Datatype.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -726,7 +726,9 @@
 
 definition
   is_none :: "'a option \<Rightarrow> bool" where
-  is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
+  is_none_none [normal post, symmetric]: "is_none x \<longleftrightarrow> x = None"
+
+lemmas [code inline] = is_none_none
 
 lemma is_none_code [code]:
   shows "is_none None \<longleftrightarrow> True"
diff -r c1836b14c63a -r 8a5412121687 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -228,7 +228,7 @@
 lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
   unfolding not_le .
 
-(* min/max *)
+text {* min/max *}
 
 definition
   min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
@@ -822,6 +822,7 @@
   "True < b \<longleftrightarrow> False"
   unfolding le_bool_def less_bool_def by simp_all
 
+
 subsection {* Monotonicity, syntactic least value operator and min/max *}
 
 locale mono =
diff -r c1836b14c63a -r 8a5412121687 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Sum_Type.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -7,7 +7,7 @@
 header{*The Disjoint Sum of Two Types*}
 
 theory Sum_Type
-imports Product_Type
+imports Typedef Fun
 begin
 
 text{*The representations of the two injections*}
diff -r c1836b14c63a -r 8a5412121687 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Test and examples for new class package *}
+header {* Test and examples for Isar class package *}
 
 theory Classpackage
 imports Main
@@ -328,6 +328,7 @@
 instance * :: (group_comm, group_comm) group_comm
 by default (simp_all add: split_paired_all mult_prod_def comm)
 
+ 
 definition
   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
 definition
diff -r c1836b14c63a -r 8a5412121687 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Mar 09 08:45:55 2007 +0100
@@ -150,14 +150,16 @@
            (*rhs' == rhs*)   Thm.symmetric rhs_conv];
         val lthy4 = case some_class
          of SOME class => 
-              LocalTheory.raw_theory
+              lthy3
+              |> LocalTheory.raw_theory
                 (ClassPackage.add_def_in_class lthy3 class
-                  ((c, mx), ((name, atts), (rhs, eq)))) lthy3
+                  ((c, mx), ((name, atts), (rhs, eq))))
           | _ => lthy3;
       in ((lhs, ((name', atts), [([eq], [])])), lthy4) end;
 
     val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
     val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
+
   in (lhss ~~ map (apsnd the_single) res, lthy'') end;
 
 end;