test/Tools/isac/Knowledge/polyminus.sml
changeset 60278 343efa173023
parent 60242 73ee61385493
child 60324 5c7128feb370
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -567,7 +567,7 @@
     1.4  
     1.5  "--- does the respective prls rewrite ?";
     1.6  val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty 
     1.7 -	     [Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
     1.8 +	     [Eval ("Poly.is_polyexp", eval_is_polyexp ""),
     1.9  	      Eval ("Prog_Expr.matchsub", eval_matchsub ""),
    1.10  	      Thm ("or_true",@{thm or_true}),
    1.11  	      (*"(?a | True) = True"*)