--- a/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 09 16:47:03 2010 +0100
@@ -171,21 +171,21 @@
text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")