[squash] assms instead of asms

docs/arch-split.md

@@ -542,13 +542,13 @@ context Arch begin global_naming ARM
    to which we'll add lemmas which will be needed to discharge
    the assumptions of the Retype_AI locale. *)
 
-named_theorems Retype_AI_asms
+named_theorems Retype_AI_assms
 
 (* We prove a lemma which matches an assumption of the Retype_AI locale,
    making use of an arch-specific definition.
-   We declare the lemma as a memory of the Retype_AI_asms collection. *)
+   We declare the lemma as a memory of the Retype_AI_assms collection. *)
 
-lemma clearMemoryVM_return[simp, Retype_AI_asms]:
+lemma clearMemoryVM_return[simp, Retype_AI_assms]:
   "clearMemoryVM a b = return ()"
   by (simp add: clearMemoryVM_def)
 
@@ -565,7 +565,7 @@ end
 global_interpretation Retype_AI?: Retype_AI
   proof goal_cases
   interpret Arch .
-  case 1 show ?case by (intro_locales; (unfold_locales; fact Retype_AI_asms)?)
+  case 1 show ?case by (intro_locales; (unfold_locales; fact Retype_AI_assms)?)
   qed
 
 (* ... *)
@@ -614,30 +614,30 @@ This allows instantiation of the locales in stages in the arch-specific theory
 
 context Arch begin global_naming ARM
 
-lemma AA[Foo_AI_asms]: "XXX"
+lemma AA[Foo_AI_assms]: "XXX"
   by (* ... *)
 
 end
 
 interpretation Foo_AI_1?: Foo_AI_1
   proof goal_cases
   interpret Arch .
-  case 1 show ?case by (intro_locales; (unfold_locales; fact Foo_AI_asms)?)
+  case 1 show ?case by (intro_locales; (unfold_locales; fact Foo_AI_assms)?)
   qed
 
 (* now we get access to GB in the global context *)
 
 context Arch begin global_naming ARM
 
-lemma AC[Foo_AI_asms]: "XXX"
+lemma AC[Foo_AI_assms]: "XXX"
   by (* using GB *)
 
 end
 
 interpretation Foo_AI_2?: Foo_AI_2
   proof goal_cases
   interpret Arch .
-  case 1 show ?case by (intro_locales; (unfold_locales; fact Foo_AI_asms)?)
+  case 1 show ?case by (intro_locales; (unfold_locales; fact Foo_AI_assms)?)
   qed
 
 (* now we get access to GD in the global context *)