| changeset 69597 | ff784d5a5bfb |
| parent 67613 | ce654b0e6d69 |
| child 76287 | cdc14f94c754 |
--- a/src/HOL/Auth/Guard/Guard_Public.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/Auth/Guard/Guard_Public.thy Sat Jan 05 17:24:33 2019 +0100 @@ -30,7 +30,7 @@ lemma agt_pubK [simp]: "agt (pubK A) = A" by (simp add: agt_def) -subsubsection\<open>basic facts about @{term initState}\<close> +subsubsection\<open>basic facts about \<^term>\<open>initState\<close>\<close> lemma no_Crypt_in_parts_init [simp]: "Crypt K X \<notin> parts (initState A)" by (cases A, auto simp: initState.simps)