--- a/src/HOL/Algebra/abstract/Ideal2.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Fri Aug 12 14:45:50 2011 -0700
@@ -25,7 +25,7 @@
text {* Principle ideal domains *}
class pid =
- assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
+ assumes pid_ax: "is_ideal (I :: ('a::domain) set) \<Longrightarrow> is_pideal I"
(* is_ideal *)
--- a/src/HOL/Auth/Message.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Auth/Message.thy Fri Aug 12 14:45:50 2011 -0700
@@ -841,7 +841,7 @@
apply (erule analz.induct, auto)
apply (blast dest:parts.Body)
apply (blast dest: parts.Body)
-apply (metis Un_absorb2 keyfree_KeyE mem_def parts_Un parts_keyfree sup1I2)
+apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
done
subsection{*Tactics useful for many protocol proofs*}
--- a/src/HOL/IMP/Util.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/IMP/Util.thy Fri Aug 12 14:45:50 2011 -0700
@@ -22,7 +22,7 @@
definition
"show" :: "string set \<Rightarrow> string list" where
- "show S = filter S letters"
+ "show S = filter (\<lambda>x. x \<in> S) letters"
value "show {''x'', ''z''}"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 12 14:45:50 2011 -0700
@@ -411,7 +411,7 @@
definition Heap_ord :: "'a Heap \<Rightarrow> 'a Heap \<Rightarrow> bool" where
"Heap_ord = img_ord execute (fun_ord option_ord)"
-definition Heap_lub :: "('a Heap \<Rightarrow> bool) \<Rightarrow> 'a Heap" where
+definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
"Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
interpretation heap!: partial_function_definitions Heap_ord Heap_lub
--- a/src/HOL/Induct/Com.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Induct/Com.thy Fri Aug 12 14:45:50 2011 -0700
@@ -84,11 +84,13 @@
lemma [pred_set_conv]:
"((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
- by (auto simp add: le_fun_def le_bool_def mem_def)
+ unfolding subset_eq
+ by (auto simp add: le_fun_def le_bool_def)
lemma [pred_set_conv]:
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
- by (auto simp add: le_fun_def le_bool_def mem_def)
+ unfolding subset_eq
+ by (auto simp add: le_fun_def le_bool_def)
text{*Command execution is functional (deterministic) provided evaluation is*}
theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Aug 12 14:45:50 2011 -0700
@@ -1436,7 +1436,7 @@
apply (rule setsum_cong2) by (simp del: replicate.simps)
also have "\<dots> = n" using i by (simp add: setsum_delta)
finally
- have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def
+ have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
by blast
then have "?xs \<in> ?A" using nxs by blast}
ultimately show ?thesis by auto
--- a/src/HOL/Matrix/Matrix.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/Matrix/Matrix.thy Fri Aug 12 14:45:50 2011 -0700
@@ -8,7 +8,7 @@
type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
-definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
+definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where
"nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
--- a/src/HOL/ex/Execute_Choice.thy Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/ex/Execute_Choice.thy Fri Aug 12 14:45:50 2011 -0700
@@ -26,7 +26,7 @@
case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
next
case False
- then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def fun_eq_iff mem_def keys_def)
+ then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def)
then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
(\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"