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.
a possibly (?) more perspicous simprule in the "simpset" part
authorpaulson
Mon, 20 Mar 2000 10:26:34 +0100
changeset 8524 f990040535c9
parent 8523 7ffc94f2f42d
child 8525 209eb2db72e6
a possibly (?) more perspicous simprule in the "simpset" part
src/HOL/ex/Qsort.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/Qsort.thy	Mon Mar 20 10:24:07 2000 +0100
+++ b/src/HOL/ex/Qsort.thy	Mon Mar 20 10:26:34 2000 +0100
@@ -10,7 +10,7 @@
 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
 
 recdef qsort "measure (size o snd)"
-    simpset "simpset() addsimps [less_Suc_eq_le]"
+    simpset "simpset() addsimps [length_filter RS le_less_trans]"
     
     "qsort(le, [])   = []"
isabelle