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/Tools/Function/lexicographic_order.ML
changeset 82299 a0693649e9c6
parent 81940 35d243b25ae2
child 82300 838f29a19f48 
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Mar 17 16:29:48 2025 +0100
@@ -203,7 +203,7 @@
           st |>
           (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
             THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
-            THEN (resolve_tac ctxt @{thms wf_empty} 1)
+            THEN (resolve_tac ctxt @{thms wf_on_def} 1)
             THEN EVERY (map (prove_row_tac ctxt) clean_table))
         end
   end) 1 st;
isabelle