diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/InsSort.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/InsSort.ML	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,77 @@
+(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
+
+Proving equations for primrec function(s) "InsSort.foldr" ...
+GC #1.17.30.54.345.21479:   (10 ms)
+*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
+*** imposes additional sort constraints on the declared type of the constant
+*** The error(s) above occurred in definition "InsSort.ins.ins_list_def"
+*)
+
+(* tools for insertion sort
+   use"Knowledge/InsSort.ML";
+*)
+
+(** interface isabelle -- isac **)
+
+theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
+
+(** rule set **)
+
+val ins_sort = prep_rls(
+  Rls{preconds = [], rew_ord = ("tless_true",tless_true),
+      rules = [Thm ("foldr_base",(*num_str*) foldr_base),
+	       Thm ("foldr_rec",foldr_rec),
+	       Thm ("ins_base",ins_base),
+	       Thm ("ins_rec",ins_rec),
+	       Thm ("sort_def",sort_def),
+
+	       Calc ("op <",eval_equ "#less_"),
+	       Thm ("if_True", if_True),
+	       Thm ("if_False", if_False)
+	       ],
+      scr = Script ((term_of o the o (parse thy)) 
+      "empty_script")
+      }:rls);      
+
+(** problem type **)
+
+store_pbt
+ (prep_pbt InsSort.thy
+ (["functional"]:pblID,
+  [("#Given" ,["unsorted u_"]),
+   ("#Find"  ,["sorted s_"])
+  ],
+  []));
+
+store_pbt
+ (prep_pbt InsSort.thy
+ (["inssort","functional"]:pblID,
+  [("#Given" ,["unsorted u_"]),
+   ("#Find"  ,["sorted s_"])
+  ],
+  []));
+
+(** method, 
+    todo: implementation needs extra object-level lists **)
+
+store_met
+ (prep_met Diff.thy
+ (["InsSort"],
+   [],
+   {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
+    crls = Atools_rls, nrls=norm_Rational
+    (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
+store_met
+ (prep_met InsSort.thy (*test-version for [#1,#3,#2] only: see *.sml*)
+ (["InsSort""sort"]:metID,
+   [("#Given" ,["unsorted u_"]),
+    ("#Find"  ,["sorted s_"])
+    ],
+   {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
+    crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
+   "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
+  ));
+
+ruleset' := overwritelthy thy (!ruleset',
+			[(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
+			 ]:(string * rls) list);