Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/DFA/Kildall.thy
changeset 80322 b10f7c981df6
parent 72184 881bd98bddee 
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -399,7 +399,7 @@
 \<comment> \<open>Well-foundedness of the termination relation:\<close>
 apply (rule wf_lex_prod)
  apply (insert orderI [THEN acc_le_listI])
- apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
+ apply (simp add: acc_def lesssub_def wfp_wf_eq [symmetric])
 apply (rule wf_finite_psubset) 
 
 \<comment> \<open>Loop decreases along termination relation:\<close>
isabelle