Updates for improved substitution method.

isabelle-utp · Jan 14, 2025 · d3536a0 · d3536a0
1 parent eb0e9ee
commit d3536a0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/utp_hoare.thy b/utp_hoare.thy
@@ -109,7 +109,7 @@ proof (rule mu_rec_total_utp_rule[OF WF M , of _ e ], goal_cases)
   case (1 st)
   then show ?case 
     using induct_step[unfolded hoare_r_def, of st "(p\<^sup>< \<and> (e\<^sup><, \<guillemotleft>st\<guillemotright>) \<in> \<guillemotleft>R\<guillemotright> \<longrightarrow> q\<^sup>>)\<^sub>e"]
-      by (simp add: usubst, simp add: subst_app_def)
+      by subst_eval
 qed
 
 lemma mu_hoare_r':