Merge branch 'popl2025_updated' of github.com:jvanbruegge/binder_datatypes into popl2025_updated

Author: Andrei Popescu

html/Binders/.browser_info/build_uuid

@@ -1 +1 @@
-785da145-7f99-4401-8912-50097c36170b
+2aae4740-5a4c-458c-b26c-cca8e1759a7e

html/Binders/MRBNF_FP.html

@@ -27,6 +27,18 @@ <h1>Theory MRBNF_Recursor</h1>
 
 </span><span class="keyword1"><span class="command"><span>declare</span></span></span><span> </span><span class="main"><span>[</span></span><span class="main"><span>[</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/inductive.ML.html#Inductive.inductive_internals|attribute"><span class="operator"><span>inductive_internals</span></span></a><span class="main"><span>]</span></span><span class="main"><span>]</span></span><span>
 
+</span><span class="keyword1"><span class="command"><span>named_theorems</span></span></span><span> </span><span class="entity_def" id="MRBNF_Recursor.equiv|attribute"><span class="entity_def" id="MRBNF_Recursor.equiv|fact"><span>equiv</span></span></span><span>
+</span><span class="keyword1"><span class="command"><span>named_theorems</span></span></span><span> </span><span class="entity_def" id="MRBNF_Recursor.equiv_commute|attribute"><span class="entity_def" id="MRBNF_Recursor.equiv_commute|fact"><span>equiv_commute</span></span></span><span>
+</span><span class="keyword1"><span class="command"><span>named_theorems</span></span></span><span> </span><span class="entity_def" id="MRBNF_Recursor.equiv_simps|attribute"><span class="entity_def" id="MRBNF_Recursor.equiv_simps|fact"><span>equiv_simps</span></span></span><span>
+
+</span><span class="keyword1"><span class="command"><span>declare</span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.Un_iff|fact"><span>Un_iff</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.de_Morgan_disj|fact"><span>de_Morgan_disj</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+  </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.inj_image_mem_iff|fact"><span>inj_image_mem_iff</span></a><span class="main"><span>[</span></span><span class="operator"><span>OF</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.bij_is_inj|fact"><span>bij_is_inj</span></a><span class="main"><span>,</span></span><span> </span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+  </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.singleton_iff|fact"><span>singleton_iff</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.image_empty|fact"><span>image_empty</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+  </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.Int_Un_distrib|fact"><span>Int_Un_distrib</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.Un_empty|fact"><span>Un_empty</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+  </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.image_is_empty|fact"><span>image_is_empty</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.image_Int|fact"><span>image_Int</span></a><span class="main"><span>[</span></span><span class="operator"><span>OF</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.bij_is_inj|fact"><span>bij_is_inj</span></a><span class="main"><span>,</span></span><span> </span><span class="operator"><span>symmetric</span></span><span class="main"><span>,</span></span><span> </span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+  </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.inj_eq|fact"><span>inj_eq</span></a><span class="main"><span>[</span></span><span class="operator"><span>OF</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.bij_is_inj|fact"><span>bij_is_inj</span></a><span class="main"><span>,</span></span><span> </span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.inj_eq|fact"><span>inj_eq</span></a><span class="main"><span>[</span></span><span class="operator"><span>OF</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Fun.html#Fun.bij_is_inj|fact"><span>bij_is_inj</span></a><span class="main"><span>,</span></span><span> </span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+  </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.image_insert|fact"><span>image_insert</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Set.html#Set.insert_iff|fact"><span>insert_iff</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span> </span><a class="entity_ref" href="MRBNF_FP.html#MRBNF_FP.notin_empty_eq_True|fact"><span>notin_empty_eq_True</span></a><span class="main"><span>[</span></span><a class="entity_ref" href="MRBNF_Recursor.html#MRBNF_Recursor.equiv_simps|attribute"><span class="operator"><span>equiv_simps</span></span></a><span class="main"><span>]</span></span><span>
+
 </span><span class="keyword1"><span class="command"><span>context</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>begin</span></span></span><span>
 </span><span class="keyword1"><span class="command"><span>ML_file</span></span></span><span> </span><span class="quoted"><a href="Tools/binder_induction.ML.html"><span>‹../Tools/binder_induction.ML›</span></a></span><span>
 </span><span class="keyword2"><span class="keyword"><span>end</span></span></span><span>
@@ -37,7 +49,8 @@ <h1>Theory MRBNF_Recursor</h1>
 
 </span><span class="keyword1"><span class="command"><span>ML_file</span></span></span><span> </span><span class="quoted"><a href="Tools/parser.ML.html"><span>"../Tools/parser.ML"</span></a></span><span>
 
-</span><span class="keyword2"><span class="keyword"><span>end</span></span></span></pre>
+</span><span class="keyword2"><span class="keyword"><span>end</span></span></span><span>
+</span></pre>
 </body>
 
 </html>

html/Binders/MRBNF_Recursor.html

@@ -3,13 +3,13 @@
 <html xmlns="http://www.w3.org/1999/xhtml">
 
 <head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"/><link rel="stylesheet" type="text/css" href="isabelle.css"/>
-<title>File ‹../Tools/binder_induction.ML›</title>
+<title>File ‹Tools/binder_induction.ML›</title>
 </head>
 
 
 <body>
 <div class="head">
-<h1>File ‹../Tools/binder_induction.ML›</h1>
+<h1>File ‹Tools/binder_induction.ML›</h1>
 </div>
 
 <pre class="source"><span class="keyword1"><span class="keyword"><span>structure</span></span></span><span> </span><span class="entity"><span>Binder_Induction</span></span><span> </span><span class="main"><span>=</span></span><span>