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/ex/AVL.ML
changeset 13601 fd3e3d6b37b2
parent 13187 e5434b822a96 
--- a/src/HOL/ex/AVL.ML	Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/ex/AVL.ML	Mon Sep 30 16:14:02 2002 +0200
@@ -133,8 +133,7 @@
  by (fast_tac (claset() addss simpset()) 1);
 by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
  by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
- by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
- by (fast_tac (claset() addss simpset()) 1);
+ by (fast_tac (claset() addss (simpset() addsimps [max_def])) 1);
 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
 by (fast_tac (claset() addss simpset()) 1);
 qed_spec_mp "height_insert";
isabelle