src/Tools/isac/Knowledge/LinEq.thy
changeset 55444 ede4248a827b
parent 55442 dd86917c35c9
child 59269 1da53d1540fe
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Fri Jun 13 09:55:49 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Fri Jun 13 10:29:06 2014 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
     1.5  ML {*
     1.6      
     1.7 -val LinPoly_simplify = prep_rls(
     1.8 +val LinPoly_simplify = prep_rls'(
     1.9    Rls {id = "LinPoly_simplify", preconds = [], 
    1.10         rew_ord = ("termlessI",termlessI), 
    1.11         erls = LinEq_erls, 
    1.12 @@ -99,7 +99,7 @@
    1.13  ML {*
    1.14  
    1.15  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.16 -val LinEq_simplify = prep_rls(
    1.17 +val LinEq_simplify = prep_rls'(
    1.18  Rls {id = "LinEq_simplify", preconds = [],
    1.19       rew_ord = ("e_rew_ord",e_rew_ord),
    1.20       erls = LinEq_erls,