test/Tools/isac/ProgLang/termC.sml
changeset 59550 2e7631381921
parent 59549 e0e3d41ef86c
child 59551 6ea6d9c377a0
     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";