Mercurial Mercurial > repos > isabelle / comparison
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/ex/InSort.ML
changeset 1750 817a34a54fb0
parent 1465 5d7a7e439cec
child 1820 e381e1c51689
equal deleted inserted replaced
1749:8968b2096011 1750:817a34a54fb0 
    38 Addsimps [result()];
 
    38 Addsimps [result()];
 
    39 
    39 
    40 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
 
    40 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
 
    41 by(list.induct_tac "xs" 1);
 
    41 by(list.induct_tac "xs" 1);
 
    42 by(ALLGOALS Asm_simp_tac);
 
    42 by(ALLGOALS Asm_simp_tac);
 
    43 result();
 
    43 qed "sorted_insort";
 
       
    44
isabelle