diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/InsSort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/InsSort.thy	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,63 @@
+(* 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 (@@@)"
+*)
+
+(* insertion sort, would need lists different from script-lists WN.11.00
+WN.7.5.03: -"- started with someList :: 'a list => unl, fun dest_list
+WN.8.5.03: error (@@@) remained with outcommenting foldr ?!?
+
+ use_thy_only"Knowledge/InsSort";
+
+*)
+
+InsSort = Script +
+
+consts
+
+(*foldr      :: [['a,'b] => 'a, 'b list, 'a] => 'a
+WN.8.5.03: already defined in Isabelle2002 (instantiated by Typefix):
+     "[[real, real] => real, real list, real] => real") : term
+
+ val t = str2term "foldr";
+val t =
+  Const
+    ("List.foldr",
+     "[[RealDef.real, RealDef.real] => RealDef.real, RealDef.real List.list,
+      RealDef.real] => RealDef.real") : term
+ *)
+  ins        :: ['a list,'a] => 'a list
+  sort       :: 'a list => 'a list
+
+(*descriptions, script-id*)
+  unsorted   :: 'a list => unl
+  sorted     :: 'a list => unl
+
+(*subproblem and script-name*)
+  Ins'_sort  :: "['a list, \
+		  \ 'a list] => 'a list"
+               ("((Script Ins'_sort (_ =))// \
+		  \ (_))" 9)
+  Sort       :: "['a list, \
+		  \ 'a list] => 'a list"
+               ("((Script Sort (_ =))// \
+		  \ (_))" 9)
+
+(*primrec
+  foldr_base "foldr f [] a = a"
+  foldr_rec  "foldr f (x#xs) a = foldr f xs (f a x)"
+*)
+
+rules
+
+(*primrec .. outcommented analoguous to ListC.thy*)
+  ins_base   "ins [] a = [a]"
+  ins_rec    "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))" 
+ 
+  sort_def   "sort ls = foldr ins ls []"
+
+end