ex/Qsort.ML

 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
 result();
 
 
 goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
 val ss = ss addsimps [result()];
 
 goal Qsort.thy
  "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac ss));
 val ss = ss addsimps [result()];
 
 goal HOL.thy "((~P --> Q) & (P --> Q)) = Q";
 by(fast_tac HOL_cs 1);

 val ss = ss addsimps [result()];
 
 goal Qsort.thy
  "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \
 \                     (Alls x:xs. Alls y:ys. le(x,y)))";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac ss));
 val ss = ss addsimps [result()];
 
 goal Qsort.thy 
  "!!le. [| total(le); transf(le) |] ==>  sorted(le,qsort(le,xs))";

 val ss = ss addsimps [result()];
 
 goal Qsort.thy
  "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \
 \                     (!x. x mem xs --> (!y. y mem ys --> le(x,y))))";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
 goal Qsort.thy