# HG changeset patch
# User paulson
# Date 952947761 -3600
# Node ID 6c6a5410a9bdb86a5394fdf652b85c0625e88afa
# Parent  7156b8e26a172cc469c5577b95737a7a58218fab
renamed "f" to "le" and "mset" to "multiset"

diff -r 7156b8e26a17 -r 6c6a5410a9bd src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Mon Mar 13 12:42:05 2000 +0100
+++ b/src/HOL/ex/InSort.ML	Mon Mar 13 12:42:41 2000 +0100
@@ -6,33 +6,32 @@
 Correctness proof of insertion sort.
 *)
 
-Goal "!y. mset(ins f x xs) y = mset (x#xs) y";
+Goal "!y. multiset(ins le x xs) y = multiset (x#xs) y";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mset_ins";
-Addsimps [mset_ins];
+by Auto_tac;
+qed_spec_mp "multiset_ins";
+Addsimps [multiset_ins];
 
-Goal "!x. mset(insort f xs) x = mset xs x";
+Goal "!x. multiset(insort le xs) x = multiset xs x";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "insort_permutes";
+by Auto_tac;
+qed_spec_mp "insort_permutes";
 
-Goal "set(ins f x xs) = insert x (set xs)";
-by (asm_simp_tac (simpset() addsimps [set_via_mset]) 1);
+Goal "set(ins le x xs) = insert x (set xs)";
+by (asm_simp_tac (simpset() addsimps [set_via_multiset]) 1);
 by (Fast_tac 1);
 qed "set_ins";
 Addsimps [set_ins];
 
-val prems = goalw InSort.thy [total_def,transf_def]
-  "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
+Goal "total(le) --> transf(le) --> sorted le (ins le x xs) = sorted le xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (cut_facts_tac prems 1);
-by (Fast_tac 1);
-qed "sorted_ins";
+by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
+by (Blast_tac 1);
+qed_spec_mp "sorted_ins";
 Addsimps [sorted_ins];
 
-Goal "[| total(f); transf(f) |] ==>  sorted f (insort f xs)";
+Goal "[| total(le); transf(le) |] ==>  sorted le (insort le xs)";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
 qed "sorted_insort";
diff -r 7156b8e26a17 -r 6c6a5410a9bd src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Mon Mar 13 12:42:05 2000 +0100
+++ b/src/HOL/ex/InSort.thy	Mon Mar 13 12:42:41 2000 +0100
@@ -13,10 +13,10 @@
   insort :: [['a,'a]=>bool, 'a list] => 'a list
 
 primrec
-  "ins f x [] = [x]"
-  "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
+  "ins le x [] = [x]"
+  "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"
 primrec
-  "insort f [] = []"
-  "insort f (x#xs) = ins f x (insort f xs)"
+  "insort le [] = []"
+  "insort le (x#xs) = ins le x (insort le xs)"
 end