(* 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);