--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sat Mar 15 22:07:29 2008 +0100
@@ -322,7 +322,7 @@
apply (frule is_type_pTs [OF wf], assumption+)
apply clarify
apply (drule rule [OF wf], assumption+)
- apply (rule refl)
+ apply (rule HOL.refl)
apply assumption+
done
qed
--- a/src/HOL/NumberTheory/EvenOdd.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy Sat Mar 15 22:07:29 2008 +0100
@@ -249,7 +249,7 @@
lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
==> ((-1::int)^j = (-1::int)^k)"
- using neg_one_power [of j] and insert neg_one_power [of k]
+ using neg_one_power [of j] and ListMem.insert neg_one_power [of k]
by (auto simp add: one_not_neg_one_mod_m zcong_sym)
end
--- a/src/HOL/NumberTheory/Gauss.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Sat Mar 15 22:07:29 2008 +0100
@@ -51,7 +51,7 @@
using p_g_2 by auto
lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
- using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
+ using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
lemma p_minus_one_l: "(p - 1) div 2 < p"
proof -
--- a/src/HOL/Word/WordBitwise.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/Word/WordBitwise.thy Sat Mar 15 22:07:29 2008 +0100
@@ -443,7 +443,7 @@
lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size]
lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq
- word_of_int [symmetric] of_int_power]
+ word_of_int [symmetric] Int.of_int_power]
lemma uint_2p:
"(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
--- a/src/HOL/Word/WordShift.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/Word/WordShift.thy Sat Mar 15 22:07:29 2008 +0100
@@ -1093,7 +1093,7 @@
lemma word_rsplit_empty_iff_size:
"(word_rsplit w = []) = (size w = 0)"
unfolding word_rsplit_def bin_rsplit_def word_size
- by (simp add: bin_rsplit_aux_simp_alt Let_def split: split_split)
+ by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
lemma test_bit_rsplit:
"sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==>
--- a/src/ZF/UNITY/AllocImpl.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Sat Mar 15 22:07:29 2008 +0100
@@ -1,4 +1,4 @@
-(*Title: ZF/UNITY/AllocImpl
+(* Title: ZF/UNITY/AllocImpl.thy
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2002 University of Cambridge
@@ -124,7 +124,8 @@
(** Safety property: (28) **)
lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
-apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def
+ Increasing.increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
apply (auto dest: ActsD)
apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
apply auto
--- a/src/ZF/UNITY/ClientImpl.thy Sat Mar 15 22:07:28 2008 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Sat Mar 15 22:07:29 2008 +0100
@@ -121,7 +121,7 @@
"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))"
apply (unfold guar_def)
apply (auto intro!: increasing_imp_Increasing
- simp add: client_prog_ok_iff increasing_def preserves_imp_prefix)
+ simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
apply (safety, force, force)+
done