Fix a shadowed lemma name

HOL-Theorem-Prover · Sep 5, 2023 · 398e682 · 398e682
1 parent 5687562
commit 398e682
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml
@@ -787,7 +787,7 @@ Proof
   metis_tac[strip_tau_rules,itree_wbisim_rules]
 QED
 
-Theorem itree_wbisim_tau:
+Theorem itree_wbisim_tau_eq:
   itree_wbisim (Tau t) t
 Proof
   ‘!t t'. t = Tau t' \/ t = t' ==> itree_wbisim t t'’ suffices_by metis_tac[] \\