1.1 --- a/test/Tools/isac/Test_Rational2.thy	Thu May 24 18:40:07 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,11 +0,0 @@
     1.4 -(* Title:  run tests on Rational2
     1.5 -   Copyright (c) Diana Meindl 2011
     1.6 -*)
     1.7 -
     1.8 -theory Test_Rational2 imports "../../../src/Tools/isac/Knowledge/Rational2" 
     1.9 -uses ("../../../src/Tools/isac/Knowledge/rational2.sml")
    1.10 -
    1.11 -begin
    1.12 -use "../../../test/Tools/isac/Knowledge/rational2.sml"
    1.13 -end
    1.14 -

     2.1 --- a/test/Tools/isac/Test_Some.thy	Thu May 24 18:40:07 2012 +0200
     2.2 +++ b/test/Tools/isac/Test_Some.thy	Thu May 24 19:07:15 2012 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  *}
     2.5  ML {*
     2.6  *}
     2.7 -ML {* (*================== --> test/../inform.sml*)
     2.8 +text {* (*================== --> test/../inform.sml*)
     2.9  "--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
    2.10  "--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
    2.11  "--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
    2.12 @@ -66,7 +66,7 @@
    2.13  "~~~~~ fun is_exactly_equal, args:"; val () = ();
    2.14  
    2.15  *}
    2.16 -ML {*
    2.17 +text {*
    2.18  print_depth 999;
    2.19  get_obj g_tac pt (lev_on p);
    2.20  print_depth 999;
    2.21 @@ -88,44 +88,6 @@
    2.22  Thm.derivation_name;
    2.23  *}
    2.24  ML {* (*================== already in code*)
    2.25 -fun thm'_of_thm thm =
    2.26 -  ((thyID_of_derivation_name o Thm.get_name_hint) thm,
    2.27 -   (thmID_of_derivation_name o Thm.get_name_hint) thm): thm'
    2.28 -fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
    2.29 -  let
    2.30 -    val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
    2.31 -    val (pt,c) = 
    2.32 -      case subs_opt of
    2.33 -        NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    2.34 -          (Rewrite thm') (f', asm) Inconsistent
    2.35 -      | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    2.36 -          (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
    2.37 -    val pt = update_branch pt p TransitiveB
    2.38 -  in (pt, (p,Res)) end
    2.39 -*}
    2.40 -text {*
    2.41 -Rewrite_Inst' (theory', rew_ord', rls, bool, subst, thm', term, (res, term list))
    2.42 -*}
    2.43 -ML {*
    2.44 -fun requestFillformula cI (errpatID, fillpatID) =
    2.45 -  let
    2.46 -    val ((pt, _), _) = get_calc cI
    2.47 -		    val pos as (p, _) = get_pos cI 1
    2.48 -    val fillforms = find_fillpatterns (pt, pos) errpatID 
    2.49 -  in
    2.50 -    case filter ((curry op = fillpatID) o 
    2.51 -        (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
    2.52 -      (_, fillform, thm, sube_opt) :: _ =>
    2.53 -        let
    2.54 -          val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
    2.55 -            (fillform, []) (get_loc pt pos) (lev_on p, Und) pt
    2.56 -        in
    2.57 -          (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
    2.58 -           autocalculateOK2xml cI pos pos' pos')
    2.59 -        end
    2.60 -    | _ => autocalculateERROR2xml cI "no fillpattern found"    
    2.61 -  end;    
    2.62 -
    2.63  *}
    2.64  ML {*
    2.65  *}