From 635bc0f990809dd2ce1dadb4180df35a8f7ffcd4 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Mon, 26 Dec 2016 11:43:16 +0000
Subject: [PATCH] Import of current (Isabelle 2016-1) release of UPF.

---
 Monads.thy                         | 4 ++--
 Normalisation.thy                  | 4 ++--
 NormalisationTestSpecification.thy | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Monads.thy b/Monads.thy
index 86eec36..634e9e7 100644
--- a/Monads.thy
+++ b/Monads.thy
@@ -512,10 +512,10 @@ lemma assert_disch3 :" \<not> P \<sigma> \<Longrightarrow> \<not> (\<sigma> \<Tu
   by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
 
 lemma assert_D : "(\<sigma> \<Turnstile> (x \<leftarrow> assert\<^sub>S\<^sub>E P; M x)) \<Longrightarrow> P \<sigma> \<and> (\<sigma> \<Turnstile> (M True))"
-  by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.split_if_asm)
+  by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm)
 
 lemma assume_D : "(\<sigma> \<Turnstile> (x \<leftarrow> assume\<^sub>S\<^sub>E P; M x)) \<Longrightarrow> \<exists> \<sigma>. (P \<sigma> \<and>  \<sigma> \<Turnstile> (M ()))"
-  apply (auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.split_if_asm)
+  apply (auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.if_split_asm)
   apply (rule_tac x="Eps P" in exI)
   apply (auto)
   apply (rule_tac x="True" in exI, rule_tac x="b" in exI)
diff --git a/Normalisation.thy b/Normalisation.thy
index d87dccf..d489001 100644
--- a/Normalisation.thy
+++ b/Normalisation.thy
@@ -228,10 +228,10 @@ proof (induct p rule: rev_induct)
  case (snoc y ys) show ?case using snoc
   proof (cases "r \<in> set ys")
    case True show ?thesis using snoc True
-    by (simp add: applied_rule_rev_def split: split_if_asm)
+    by (simp add: applied_rule_rev_def split: if_split_asm)
    next
    case False show ?thesis using snoc False
-  by (simp add: applied_rule_rev_def split: split_if_asm)
+  by (simp add: applied_rule_rev_def split: if_split_asm)
  qed
 qed
 
diff --git a/NormalisationTestSpecification.thy b/NormalisationTestSpecification.thy
index 846d29b..f25862f 100644
--- a/NormalisationTestSpecification.thy
+++ b/NormalisationTestSpecification.thy
@@ -130,7 +130,7 @@ definition disjDomGD where "disjDomGD p = disjDom (butlast p)"
 lemma distrPUTLG1: "\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; PUTListGD PUT x PL\<rbrakk> \<Longrightarrow> PUT x = P x"
   apply (induct PL)  
   apply (simp_all add: domIff PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def)
-  apply (auto simp: dom_def domIff split: split_if_asm) 
+  apply (auto simp: dom_def domIff split: if_split_asm) 
 done
 
 lemma distrPUTLG2: