--- 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
--- 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
--- 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"
--- 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 =
--- 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*}
--- 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
--- 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;