equal
deleted
inserted
replaced
17 "----------- step through 'fun rewrite_terms_' ---------"; |
17 "----------- step through 'fun rewrite_terms_' ---------"; |
18 "----------- rewrite_inst_ bdvs -------------------------"; |
18 "----------- rewrite_inst_ bdvs -------------------------"; |
19 "----------- check diff 2002--2009-3 --------------------"; |
19 "----------- check diff 2002--2009-3 --------------------"; |
20 "----------- compare all prepat's existing 2010 ---------"; |
20 "----------- compare all prepat's existing 2010 ---------"; |
21 "----------- fun app_rev, Rrls, -------------------------"; |
21 "----------- fun app_rev, Rrls, -------------------------"; |
|
22 "----------- 2011 thms with axclasses -------------------"; |
22 "--------------------------------------------------------"; |
23 "--------------------------------------------------------"; |
23 "--------------------------------------------------------"; |
24 "--------------------------------------------------------"; |
24 "--------------------------------------------------------"; |
25 "--------------------------------------------------------"; |
25 |
26 |
26 |
27 |
489 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"], |
490 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"], |
490 [] : (term * term) list, erls); |
491 [] : (term * term) list, erls); |
491 case eval__true thy i asms bdv rls of |
492 case eval__true thy i asms bdv rls of |
492 ([], true) => () |
493 ([], true) => () |
493 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; |
494 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; |
|
495 |
|
496 "----------- 2011 thms with axclasses -------------------"; |
|
497 "----------- 2011 thms with axclasses -------------------"; |
|
498 "----------- 2011 thms with axclasses -------------------"; |
|
499 val thm = num_str @{thm divide_1}; |
|
500 val prop = prop_of thm; |
|
501 atomty prop; (*Type 'a*) |
|
502 val t = str2term "(2*x)/1"; (*Type real*) |
|
503 |
|
504 val (thy, ro, er, inst) = |
|
505 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
|
506 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*) |
|
507 |