Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 21 Jan 2025 16:09:51 +0100
changeset 81940 35d243b25ae2
parent 81939 07fefe59ac20
child 81941 cb8f396dd39f
tuned;
src/HOL/Tools/Function/lexicographic_order.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Function/termination.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Tue Jan 21 11:16:48 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Tue Jan 21 16:09:51 2025 +0100
@@ -76,7 +76,7 @@
         (case try_proof ctxt (goals \<^const_name>\<open>Orderings.less_eq\<close>) solve_tac of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
-            if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>] then False thm2
+            if Thm.prems_of thm2 = [\<^prop>\<open>False\<close>] then False thm2
             else None (thm2, thm)
         | _ => raise Match) (* FIXME *)
     | _ => raise Match)
--- a/src/HOL/Tools/Function/termination.ML	Tue Jan 21 11:16:48 2025 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Tue Jan 21 16:09:51 2025 +0100
@@ -179,7 +179,7 @@
         (case try \<^const_name>\<open>Orderings.less_eq\<close> of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
-            if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>]
+            if Thm.prems_of thm2 = [\<^prop>\<open>False\<close>]
             then False thm2 else None (thm2, thm)
         | _ => raise Match) (* FIXME *)
     | _ => raise Match)
isabelle