1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Wed Jul 27 16:56:45 2011 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Thu Jul 28 10:58:17 2011 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  "----------- check diff 2002--2009-3 --------------------";
     1.5  "----------- compare all prepat's existing 2010 ---------";
     1.6  "----------- fun app_rev, Rrls, -------------------------";
     1.7 +"----------- 2011 thms with axclasses -------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -491,3 +492,16 @@
    1.12  case eval__true thy i asms bdv rls of 
    1.13      ([], true) => ()
    1.14    | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
    1.15 +
    1.16 +"----------- 2011 thms with axclasses -------------------";
    1.17 +"----------- 2011 thms with axclasses -------------------";
    1.18 +"----------- 2011 thms with axclasses -------------------";
    1.19 +val thm = num_str @{thm divide_1};
    1.20 +val prop = prop_of thm;
    1.21 +atomty prop;                                     (*Type 'a*)
    1.22 +val t = str2term "(2*x)/1";                      (*Type real*)
    1.23 +
    1.24 +val (thy, ro, er, inst) = 
    1.25 +    (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
    1.26 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
    1.27 +