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/BCV/Opt.ML
changeset 10918 9679326489cd
parent 10172 3daeda3d3cd0 
--- a/src/HOL/BCV/Opt.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/BCV/Opt.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -50,7 +50,7 @@
 AddIffs [le_None];
 
 
-Goalw [Opt.sl_def,semilat_def,closed_def,split RS eq_reflection]
+Goalw [Opt.sl_def,semilat_def,closed_def, split_conv RS eq_reflection]
  "!!L. semilat L ==> semilat (Opt.sl L)";
 by (split_all_tac 1);
 by (asm_full_simp_tac (simpset() addsplits [option.split]
isabelle