# HG changeset patch
# User wenzelm
# Date 1390683124 -3600
# Node ID 378ae9e4617501d1d877566dd05ec42af64de7d3
# Parent  863b4f9f6bd7191691e89a4b7e1b6df85e970ce1
prefer explicit 'for' context;

diff -r 863b4f9f6bd7 -r 378ae9e46175 src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Sat Jan 25 18:34:05 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Sat Jan 25 21:52:04 2014 +0100
@@ -93,7 +93,7 @@
 (*Simplifying   
  parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
   This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
 
 lemma knows_Spy_Says [simp]:
      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -256,7 +256,7 @@
        knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
        knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
 
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
 
 ML
 {*
@@ -290,7 +290,7 @@
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
 
-lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
 
 ML
 {*
diff -r 863b4f9f6bd7 -r 378ae9e46175 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Sat Jan 25 18:34:05 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Sat Jan 25 21:52:04 2014 +0100
@@ -190,7 +190,7 @@
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
@@ -388,9 +388,9 @@
 apply (erule analz.induct, blast+)
 done
 
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -404,7 +404,7 @@
 apply (erule analz.induct, auto)
 done
 
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection{*General equational properties *}
 
@@ -786,21 +786,23 @@
 text{*Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the @{text analz_insert} rules*}
 
-lemmas pushKeys [standard] =
+lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
+  for K C N X Y K'
 
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
+  for X K C N X' Y
 
 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered. *}
diff -r 863b4f9f6bd7 -r 378ae9e46175 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sat Jan 25 18:34:05 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Jan 25 21:52:04 2014 +0100
@@ -284,8 +284,8 @@
 lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
 lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
 
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
 
 subsection {* Order instances *}