Deploying to gh-pages from @ 3ef65e5 🚀

.browser_info/build_uuid

@@ -1 +1 @@
-1768e4e2-8ea2-4c52-aad4-2ed9518d89fc
+c78a1c5d-3bac-4240-8d15-aba6eb516ed2

AOT_Axioms.html

@@ -179,10 +179,10 @@ <h1>Theory AOT_Axioms</h1>
 <a name="L112" href="#L112"><span class="linenumber">112</span></a>  </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html#HOL.rule|method"><span class="operator"><span>rule</span></span></a><span> </span><a class="entity_ref" href="AOT_model.html#AOT_model.AOT_model_axiomI|fact"><span>AOT_model_axiomI</span></a><span class="main"><span>)</span></span><span>
 <a name="L113" href="#L113"><span class="linenumber">113</span></a>     </span><span class="main"><span>(</span></span><span class="operator"><span>simp</span></span><span> </span><span class="quasi_keyword"><span>add</span></span><span class="main"><span class="main"><span>:</span></span></span><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_act|fact"><span>AOT_sem_act</span></a><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_box|fact"><span>AOT_sem_box</span></a><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_equiv|fact"><span>AOT_sem_equiv</span></a><span class="main"><span>)</span></span><span>
 <a name="L114" href="#L114"><span class="linenumber">114</span></a>
-<a name="L115" href="#L115"><span class="linenumber">115</span></a></span><span class="keyword1"><span class="command"><span>AOT_axiom</span></span></span><span> </span><span class="entity_def" id="AOT_Axioms.descriptions|fact" title="(47)"><span class="entity_def" id="AOT_Axioms.descriptions|thm" title="(47)"><span>descriptions</span></span></span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>‹</span><span class="free"><span>x</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword1"><span><span class="hidden">❙</span><b>ι</b></span></span><span class="bound"><span>x</span></span><span class="main"><span>(</span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>x</span></span><span class="main"><span>}</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="main"><span>∀</span></span><span class="bound"><span>z</span></span><span class="main"><span>(</span></span><span class="keyword1"><span><span class="hidden">❙</span><b>𝒜</b></span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>z</span></span><span class="main"><span>}</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="bound"><span>z</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="free"><span>x</span></span><span class="main"><span>)</span></span><span>›</span></span></span><span>
+<a name="L115" href="#L115"><span class="linenumber">115</span></a></span><span class="keyword1"><span class="command"><span>AOT_axiom</span></span></span><span> </span><span class="entity_def" id="AOT_Axioms.descriptions|fact" title="(47)"><span class="entity_def" id="AOT_Axioms.descriptions|thm" title="(47)"><span>descriptions</span></span></span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>‹</span><span class="free"><span>y</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword1"><span><span class="hidden">❙</span><b>ι</b></span></span><span class="bound"><span>x</span></span><span class="main"><span>(</span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>x</span></span><span class="main"><span>}</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="main"><span>∀</span></span><span class="bound"><span>x</span></span><span class="main"><span>(</span></span><span class="keyword1"><span><span class="hidden">❙</span><b>𝒜</b></span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>x</span></span><span class="main"><span>}</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="bound"><span>x</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="free"><span>y</span></span><span class="main"><span>)</span></span><span>›</span></span></span><span>
 <a name="L116" href="#L116"><span class="linenumber">116</span></a></span><span class="keyword1"><span class="command"><span>proof</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html#HOL.rule|method"><span class="operator"><span>rule</span></span></a><span> </span><a class="entity_ref" href="AOT_model.html#AOT_model.AOT_model_axiomI|fact"><span>AOT_model_axiomI</span></a><span class="main"><span>)</span></span><span>
 <a name="L117" href="#L117"><span class="linenumber">117</span></a>  </span><span class="keyword1"><span class="command"><span>AOT_modally_strict {</span></span></span><span>
-<a name="L118" href="#L118"><span class="linenumber">118</span></a>    </span><span class="keyword3"><span class="command"><span>AOT_show</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>‹</span><span class="free"><span>x</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword1"><span><span class="hidden">❙</span><b>ι</b></span></span><span class="bound"><span>x</span></span><span class="main"><span>(</span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>x</span></span><span class="main"><span>}</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="main"><span>∀</span></span><span class="bound"><span>z</span></span><span class="main"><span>(</span></span><span class="keyword1"><span><span class="hidden">❙</span><b>𝒜</b></span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>z</span></span><span class="main"><span>}</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="bound"><span>z</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="free"><span>x</span></span><span class="main"><span>)</span></span><span>›</span></span></span><span>
+<a name="L118" href="#L118"><span class="linenumber">118</span></a>    </span><span class="keyword3"><span class="command"><span>AOT_show</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>‹</span><span class="free"><span>y</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword1"><span><span class="hidden">❙</span><b>ι</b></span></span><span class="bound"><span>x</span></span><span class="main"><span>(</span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>x</span></span><span class="main"><span>}</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="main"><span>∀</span></span><span class="bound"><span>x</span></span><span class="main"><span>(</span></span><span class="keyword1"><span><span class="hidden">❙</span><b>𝒜</b></span></span><span class="free"><span>φ</span></span><span class="main"><span>{</span></span><span class="bound"><span>x</span></span><span class="main"><span>}</span></span><span> </span><span class="main"><span>≡</span></span><span> </span><span class="bound"><span>x</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="free"><span>y</span></span><span class="main"><span>)</span></span><span>›</span></span></span><span>
 <a name="L119" href="#L119"><span class="linenumber">119</span></a>      </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Tools/induct.ML.html#HOL.induct|method"><span class="operator"><span>induct</span></span></a><span class="main"><span class="keyword3"><span>;</span></span></span><span> </span><span class="operator"><span>simp</span></span><span> </span><span class="quasi_keyword"><span>add</span></span><span class="main"><span class="main"><span>:</span></span></span><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_equiv|fact"><span>AOT_sem_equiv</span></a><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_forall|fact"><span>AOT_sem_forall</span></a><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_act|fact"><span>AOT_sem_act</span></a><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_eq|fact"><span>AOT_sem_eq</span></a><span class="main"><span>)</span></span><span>
 <a name="L120" href="#L120"><span class="linenumber">120</span></a>         </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/Metis/metis_tactic.ML.html#Metis.metis|method"><span class="operator"><span>metis</span></span></a><span> </span><span class="main"><span class="main"><span>(</span></span></span><span>no_types</span><span class="main"><span class="main"><span>,</span></span></span><span> opaque_lifting</span><span class="main"><span class="main"><span>)</span></span></span><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_desc_denotes|fact"><span>AOT_sem_desc_denotes</span></a><span> </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_desc_prop|fact"><span>AOT_sem_desc_prop</span></a><span>
 <a name="L121" href="#L121"><span class="linenumber">121</span></a>                                           </span><a class="entity_ref" href="AOT_semantics.html#AOT_semantics.AOT_sem_denotes|fact"><span>AOT_sem_denotes</span></a><span class="main"><span>)</span></span><span>