# HG changeset patch
# User huffman
# Date 1313619154 25200
# Node ID 355d5438f5fb5091155e3dd10ad9dc6ea6167a94
# Parent  e44f465c00a18439e3b6e496fc16823515e78e7f# Parent  a93426812ad5ef0765e0dcb980937e759ffb99f4
merged

diff -r a93426812ad5 -r 355d5438f5fb src/HOL/IMP/Sem_Equiv.thy
--- 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
diff -r a93426812ad5 -r 355d5438f5fb src/HOL/Library/Wfrec.thy
--- 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"
 
diff -r a93426812ad5 -r 355d5438f5fb src/HOL/Multivariate_Analysis/Determinants.thy
--- 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]