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/Data_Structures/Less_False.thy
changeset 69597 ff784d5a5bfb
parent 67406 23307fd33906
child 78099 4d9349989d94 
--- a/src/HOL/Data_Structures/Less_False.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/Less_False.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -14,7 +14,7 @@
 
     fun prove_less_False ((less as Const(_,T)) $ r $ s) =
       let val prems = Simplifier.prems_of ctxt;
-          val le = Const (@{const_name less_eq}, T);
+          val le = Const (\<^const_name>\<open>less_eq\<close>, T);
           val t = HOLogic.mk_Trueprop(le $ s $ r);
       in case find_first (prp t) prems of
            NONE =>
isabelle