src/HOL/Auth/Shared.thy

--- a/src/HOL/Auth/Shared.thy	Thu Dec 06 22:38:50 2001 +0100
+++ b/src/HOL/Auth/Shared.thy	Fri Dec 07 11:10:54 2001 +0100
@@ -57,4 +57,7 @@
             gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
     "for proving possibility theorems"
 
+lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
+by (induct e, auto simp: knows_Cons)
+
 end