1.1 --- a/src/Tools/isac/IsacKnowledge/InsSort.ML	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,77 +0,0 @@
     1.4 -(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
     1.5 -
     1.6 -Proving equations for primrec function(s) "InsSort.foldr" ...
     1.7 -GC #1.17.30.54.345.21479:   (10 ms)
     1.8 -*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
     1.9 -*** imposes additional sort constraints on the declared type of the constant
    1.10 -*** The error(s) above occurred in definition "InsSort.ins.ins_list_def"
    1.11 -*)
    1.12 -
    1.13 -(* tools for insertion sort
    1.14 -   use"IsacKnowledge/InsSort.ML";
    1.15 -*)
    1.16 -
    1.17 -(** interface isabelle -- isac **)
    1.18 -
    1.19 -theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
    1.20 -
    1.21 -(** rule set **)
    1.22 -
    1.23 -val ins_sort = prep_rls(
    1.24 -  Rls{preconds = [], rew_ord = ("tless_true",tless_true),
    1.25 -      rules = [Thm ("foldr_base",(*num_str*) foldr_base),
    1.26 -	       Thm ("foldr_rec",foldr_rec),
    1.27 -	       Thm ("ins_base",ins_base),
    1.28 -	       Thm ("ins_rec",ins_rec),
    1.29 -	       Thm ("sort_def",sort_def),
    1.30 -
    1.31 -	       Calc ("op <",eval_equ "#less_"),
    1.32 -	       Thm ("if_True", if_True),
    1.33 -	       Thm ("if_False", if_False)
    1.34 -	       ],
    1.35 -      scr = Script ((term_of o the o (parse thy)) 
    1.36 -      "empty_script")
    1.37 -      }:rls);      
    1.38 -
    1.39 -(** problem type **)
    1.40 -
    1.41 -store_pbt
    1.42 - (prep_pbt InsSort.thy
    1.43 - (["functional"]:pblID,
    1.44 -  [("#Given" ,["unsorted u_"]),
    1.45 -   ("#Find"  ,["sorted s_"])
    1.46 -  ],
    1.47 -  []));
    1.48 -
    1.49 -store_pbt
    1.50 - (prep_pbt InsSort.thy
    1.51 - (["inssort","functional"]:pblID,
    1.52 -  [("#Given" ,["unsorted u_"]),
    1.53 -   ("#Find"  ,["sorted s_"])
    1.54 -  ],
    1.55 -  []));
    1.56 -
    1.57 -(** method, 
    1.58 -    todo: implementation needs extra object-level lists **)
    1.59 -
    1.60 -store_met
    1.61 - (prep_met Diff.thy
    1.62 - (["InsSort"],
    1.63 -   [],
    1.64 -   {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    1.65 -    crls = Atools_rls, nrls=norm_Rational
    1.66 -    (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
    1.67 -store_met
    1.68 - (prep_met InsSort.thy (*test-version for [#1,#3,#2] only: see *.sml*)
    1.69 - (["InsSort""sort"]:metID,
    1.70 -   [("#Given" ,["unsorted u_"]),
    1.71 -    ("#Find"  ,["sorted s_"])
    1.72 -    ],
    1.73 -   {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
    1.74 -    crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
    1.75 -   "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
    1.76 -  ));
    1.77 -
    1.78 -ruleset' := overwritelthy thy (!ruleset',
    1.79 -			[(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
    1.80 -			 ]:(string * rls) list);