# HG changeset patch
# User paulson
# Date 1128006177 -7200
# Node ID e969fc0a492566aa11cea905f1c3775116a3a3fb
# Parent  ee5b42e3cbb4243560bce0e355ded0736dc01254
simprules need names

diff -r ee5b42e3cbb4 -r e969fc0a4925 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu Sep 29 15:50:46 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Thu Sep 29 17:02:57 2005 +0200
@@ -268,10 +268,10 @@
 lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
   by (simp add: numeral_2_eq_2 Power.power_Suc)
 
-lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
+lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
   by (simp add: power2_eq_square)
 
-lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
+lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
   by (simp add: power2_eq_square)
 
 lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
diff -r ee5b42e3cbb4 -r e969fc0a4925 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 29 15:50:46 2005 +0200
+++ b/src/HOL/List.thy	Thu Sep 29 17:02:57 2005 +0200
@@ -1774,7 +1774,7 @@
 apply blast
 done
 
-lemma [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
+lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
 apply(induct xs)
  apply simp
 apply simp
@@ -2180,7 +2180,7 @@
   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
 
-lemma [simp]: "set_Cons A {[]} = (%x. [x])`A"
+lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
 by (auto simp add: set_Cons_def)
 
 text{*Yields the set of lists, all of the same length as the argument and
diff -r ee5b42e3cbb4 -r e969fc0a4925 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Sep 29 15:50:46 2005 +0200
+++ b/src/HOL/Map.thy	Thu Sep 29 17:02:57 2005 +0200
@@ -202,7 +202,7 @@
  "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
 by(auto simp del:map_of_eq_Some_iff simp add:map_of_eq_Some_iff[symmetric])
 
-lemma [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
+lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
   \<Longrightarrow> map_of xys x = Some y"
 apply (induct xys)
  apply simp
@@ -553,13 +553,13 @@
 lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
 by(simp add:map_le_def)
 
-lemma [simp]: "f(x := None) \<subseteq>\<^sub>m f"
+lemma upd_None_map_le [simp]: "f(x := None) \<subseteq>\<^sub>m f"
 by(force simp add:map_le_def)
 
 lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
 by(fastsimp simp add:map_le_def)
 
-lemma [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
+lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
 by(force simp add:map_le_def)
 
 lemma map_le_upds[simp]: