Deploying to gh-pages from @ 81c1d54 🚀

ekpyron · Oct 5, 2023 · db369e9 · db369e9
1 parent 5c70beb
commit db369e9
Show file tree

Hide file tree

Showing 31 changed files with 17,927 additions and 15,696 deletions.
diff --git a/.browser_info/build_uuid b/.browser_info/build_uuid
@@ -0,0 +1 @@
+984ebde3-adda-44cb-a914-1acc6dd70db8
diff --git a/AOT_Axioms.html b/AOT_Axioms.html
diff --git a/AOT_BasicLogicalObjects.html b/AOT_BasicLogicalObjects.html
diff --git a/AOT_Definitions.html b/AOT_Definitions.html
diff --git a/AOT_ExtendedRelationComprehension.html b/AOT_ExtendedRelationComprehension.html
diff --git a/AOT_NaturalNumbers.html b/AOT_NaturalNumbers.html
diff --git a/AOT_PLM.html b/AOT_PLM.html
diff --git a/AOT_PossibleWorlds.html b/AOT_PossibleWorlds.html
diff --git a/AOT_RestrictedVariables.html b/AOT_RestrictedVariables.html
diff --git a/AOT_commands.html b/AOT_commands.html
diff --git a/AOT_misc.html b/AOT_misc.html
diff --git a/AOT_model.html b/AOT_model.html
diff --git a/AOT_semantics.html b/AOT_semantics.html
diff --git a/AOT_syntax.html b/AOT_syntax.html
diff --git a/ExportInfo.html b/ExportInfo.html
@@ -65,7 +65,7 @@
 <h1>Theory ExportInfo</h1>
 </div>
 
-<pre class="source"><a name="L1" href="#L1"><span class="linenumber">1</span></a><span class="keyword1"><span class="command"><span>theory</span></span></span><span> </span><span>ExportInfo</span><span>
+<pre class="source"><a name="L1" href="#L1"><span class="linenumber">1</span></a><span class="keyword1"><span class="command"><span>theory</span></span></span><span> </span><a href="ExportInfo.html"><span>ExportInfo</span></a><span>
 <a name="L2" href="#L2"><span class="linenumber">2</span></a>  </span><span class="keyword2"><span class="keyword"><span>imports</span></span></span><span> </span><a href="AOT_misc.html"><span>AOT_misc</span></a><span>
 <a name="L3" href="#L3"><span class="linenumber">3</span></a></span><span class="keyword2"><span class="keyword"><span>begin</span></span></span><span>
 <a name="L4" href="#L4"><span class="linenumber">4</span></a>
@@ -94,7 +94,7 @@ <h1>Theory ExportInfo</h1>
 <a name="L27" href="#L27"><span class="linenumber">27</span></a></span><span class="keyword2"><span class="keyword"><span>in</span></span></span><span>
 <a name="L28" href="#L28"><span class="linenumber">28</span></a></span><span>Facts.dest_all</span><span> </span><span class="main"><span>(</span></span><span>Context.Proof</span><span> </span><span class="entity"><span>ctxt</span></span><span class="main"><span>)</span></span><span> </span><span>false</span><span> </span><span class="main"><span>[</span></span><span class="main"><span>]</span></span><span> </span><span class="entity"><span>global_facts</span></span><span> </span><span>|&gt;</span><span>
 <a name="L29" href="#L29"><span class="linenumber">29</span></a>  </span><span>map</span><span> </span><span class="main"><span>(</span></span><span class="keyword1"><span class="keyword"><span>fn</span></span></span><span> </span><span class="main"><span>(</span></span><span class="entity"><span>n</span></span><span class="main"><span>,</span></span><span> </span><span class="entity"><span>thms</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><span>=&gt;</span></span><span> </span><span class="keyword2"><span class="keyword"><span>let</span></span></span><span>
-<a name="L30" href="#L30"><span class="linenumber">30</span></a>    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="main"><span>{</span></span><span>concealed</span><span> </span><span class="main"><span>=</span></span><span> </span><span class="main"><span>_</span></span><span class="main"><span>,</span></span><span> </span><span>group</span><span> </span><span class="main"><span>=</span></span><span> </span><span class="main"><span>_</span></span><span class="main"><span>,</span></span><span> </span><span>theory_long_name</span><span> </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>thy_name</span></span><span class="main"><span>,</span></span><span> </span><span>pos</span><span> </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>pos</span></span><span class="main"><span>,</span></span><span> </span><span>serial</span><span> </span><span class="main"><span>=</span></span><span> </span><span class="main"><span>_</span></span><span class="main"><span>}</span></span><span> </span><span class="main"><span>=</span></span><span>
+<a name="L30" href="#L30"><span class="linenumber">30</span></a>    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="main"><span>{</span></span><span>theory_long_name </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>thy_name</span></span><span class="main"><span>,</span></span><span> pos </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>pos</span></span><span class="main"><span>,</span></span><span> </span><span class="main"><span>...</span></span><span class="main"><span>}</span></span><span> </span><span class="main"><span>=</span></span><span>
 <a name="L31" href="#L31"><span class="linenumber">31</span></a>      </span><span>Name_Space.the_entry</span><span> </span><span class="main"><span>(</span></span><span>Facts.space_of</span><span> </span><span class="entity"><span>global_facts</span></span><span class="main"><span>)</span></span><span> </span><span class="entity"><span>n</span></span><span>
 <a name="L32" href="#L32"><span class="linenumber">32</span></a>    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>name</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span>Binding.name_of</span><span> </span><span class="main"><span>(</span></span><span>Binding.qualified_name</span><span> </span><span class="entity"><span>n</span></span><span class="main"><span>)</span></span><span>
 <a name="L33" href="#L33"><span class="linenumber">33</span></a>    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>items</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span>Symtab.keys</span><span> </span><span class="main"><span>(</span></span><span>fold</span><span> </span><span class="main"><span>(</span></span><span class="keyword1"><span class="keyword"><span>fn</span></span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span class="main"><span>=&gt;</span></span><span> </span><span class="keyword1"><span class="keyword"><span>fn</span></span></span><span> </span><span class="entity"><span>set</span></span><span> </span><span class="main"><span>=&gt;</span></span><span>
@@ -115,7 +115,7 @@ <h1>Theory ExportInfo</h1>
 <a name="L48" href="#L48"><span class="linenumber">48</span></a></span><span class="main"><span>(</span></span><span>Export.export</span><span> </span><span class="entity"><span>thy</span></span><span> </span><span class="main"><span>(</span></span><span>Path.binding0</span><span> </span><span class="main"><span>(</span></span><span>Path.make</span><span> </span><span class="main"><span>[</span></span><span class="inner_quoted"><span>"info"</span></span><span class="main"><span>]</span></span><span class="main"><span>)</span></span><span class="main"><span>)</span></span><span> </span><span class="entity"><span>blob</span></span><span class="main"><span>;</span></span><span>
 <a name="L49" href="#L49"><span class="linenumber">49</span></a> </span><span>Export.export</span><span> </span><span class="entity"><span>thy</span></span><span> </span><span class="main"><span>(</span></span><span>Path.binding0</span><span> </span><span class="main"><span>(</span></span><span>Path.make</span><span> </span><span class="main"><span>[</span></span><span class="inner_quoted"><span>"info2"</span></span><span class="main"><span>]</span></span><span class="main"><span>)</span></span><span class="main"><span>)</span></span><span> </span><span class="entity"><span>blob2</span></span><span class="main"><span>;</span></span><span> </span><span class="entity"><span>ctxt</span></span><span class="main"><span>)</span></span><span>
 <a name="L50" href="#L50"><span class="linenumber">50</span></a></span><span class="keyword2"><span class="keyword"><span>end</span></span></span><span>
-<a name="L51" href="#L51"><span class="linenumber">51</span></a></span><span>›</span></span><span>
+<a name="L51" href="#L51"><span class="linenumber">51</span></a>›</span></span><span>
 <a name="L52" href="#L52"><span class="linenumber">52</span></a>
 <a name="L53" href="#L53"><span class="linenumber">53</span></a></span><span class="keyword2"><span class="keyword"><span>end</span></span></span></pre>
 </body>