1.1 --- a/test/Tools/isac/ProgLang/termC.sml Sat Jun 01 11:09:19 2019 +0200
1.2 +++ b/test/Tools/isac/ProgLang/termC.sml Sat Jun 22 13:15:52 2019 +0200
1.3 @@ -29,6 +29,7 @@
1.4 "----------- fun dest_binop_typ ----------------------------------------------------------------";
1.5 "----------- fun is_list -----------------------------------------------------------------------";
1.6 "----------- fun inst_abs ----------------------------------------------------------------------";
1.7 +"----------- fun numbers_to_string -------------------------------------------------------------";
1.8 "--------------------------------------------------------";
1.9 "--------------------------------------------------------";
1.10
1.11 @@ -740,3 +741,13 @@
1.12 val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $ scr'_body = scr'
1.13 ;
1.14 if scr'_body = LTool.body_of original then () else error "inst_abs changed";
1.15 +
1.16 +"----------- fun numbers_to_string -------------------------------------------------------------";
1.17 +"----------- fun numbers_to_string -------------------------------------------------------------";
1.18 +"----------- fun numbers_to_string -------------------------------------------------------------";
1.19 +if numbers_to_string @{term "123::real"} = Free ("123", HOLogic.realT)
1.20 +then () else error "numbers_to_string '123' changed";
1.21 +if numbers_to_string @{term "1::real"} = Free ("1", HOLogic.realT)
1.22 +then () else error "numbers_to_string '1' changed";
1.23 +if numbers_to_string @{term "0::real"} = Free ("0", HOLogic.realT)
1.24 +then () else error "numbers_to_string '0' changed";