--- a/src/HOL/IMP/Sem_Equiv.thy Thu Aug 18 00:02:44 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy Wed Aug 17 15:12:34 2011 -0700
@@ -132,7 +132,7 @@
simp: hoare_valid_def)
lemma equiv_up_to_if:
- "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
by (auto simp: bequiv_up_to_def equiv_up_to_def)
@@ -162,4 +162,4 @@
by (blast dest: while_never)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Wfrec.thy Thu Aug 18 00:02:44 2011 +0200
+++ b/src/HOL/Library/Wfrec.thy Wed Aug 17 15:12:34 2011 -0700
@@ -76,12 +76,12 @@
subsection {* Nitpick setup *}
-axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
-definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Thu Aug 18 00:02:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Aug 17 15:12:34 2011 -0700
@@ -131,7 +131,7 @@
{fix p assume p: "p \<in> {p. p permutes ?U}"
from p have pU: "p permutes ?U" by blast
have sth: "sign (inv p) = sign p"
- by (metis sign_inverse fU p mem_def Collect_def permutation_permutes)
+ by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
from permutes_inj[OF pU]
have pi: "inj_on p ?U" by (blast intro: subset_inj_on)
from permutes_image[OF pU]