test/Tools/isac/Knowledge/poly-1.sml
changeset 60405 d4ebe139100d
parent 60340 0ee698b0a703
child 60424 c3acf9c442ac
     1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4  "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
     1.5  "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
     1.6  	    (*if*) (is_nums x) (*else*);
     1.7 -  val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
     1.8 +  val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
     1.9        (*case*) x (*of*); 
    1.10  (*+*)UnparseC.term x = "x \<up> 2";
    1.11              (*if*) TermC.is_num t (*then*);
    1.12 @@ -370,7 +370,7 @@
    1.13             counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
    1.14  "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
    1.15  	    (*if*) (is_nums x) (*else*);
    1.16 -  val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
    1.17 +  val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
    1.18        (*case*) x (*of*); 
    1.19  (*+*)UnparseC.term x = "y \<up> 2";
    1.20              (*if*) TermC.is_num t (*then*);
    1.21 @@ -385,7 +385,7 @@
    1.22  "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
    1.23  "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
    1.24  	    (*if*) (is_nums x) (*else*);
    1.25 -val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
    1.26 +val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
    1.27        (*case*) x (*of*); 
    1.28  (*+*)UnparseC.term x = "x \<up> 3";
    1.29              (*if*) TermC.is_num t (*then*);