test/Tools/isac/Specify/input-descript.sml
changeset 59953 933211a252f2
parent 59596 2d99bdf0fdaf
child 59959 0f0718c61f68
     1.1 --- a/test/Tools/isac/Specify/input-descript.sml	Fri May 08 18:30:21 2020 +0200
     1.2 +++ b/test/Tools/isac/Specify/input-descript.sml	Sat May 09 11:55:51 2020 +0200
     1.3 @@ -14,14 +14,14 @@
     1.4  "-------- distinguish input to Model ----------------------------------------------------------";
     1.5  "-------- distinguish input to Model ----------------------------------------------------------";
     1.6  "-------- distinguish input to Model ----------------------------------------------------------";
     1.7 -"----- fun is_booll_dsc -----";
     1.8 +"----- fun Input_Descript.for_bool_list -----";
     1.9  val t as Const ("Input_Descript.relations", 
    1.10    Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]), 
    1.11      Type ("Input_Descript.una", [])])) = @{term "relations"};
    1.12  atomtyp (type_of t);
    1.13 -if is_booll_dsc t then () else error "is_booll_dsc changed";
    1.14 -"----- fun is_reall_dsc -----";
    1.15 -if not (is_reall_dsc t) then () else error "is_reall_dsc changed";
    1.16 +if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed";
    1.17 +"----- fun Input_Descript.for_real -----";
    1.18 +if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed";
    1.19  
    1.20  "----- fun is_list_dsc -----";
    1.21  val t = @{term "someList"};
    1.22 @@ -33,11 +33,11 @@
    1.23  
    1.24  "----- fun is_list_dsc -----";
    1.25  val t = @{term "maximum"};
    1.26 -if is_dsc t then () else error "is_dsc changed 1";
    1.27 +if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 1";
    1.28  
    1.29  val t = head_of @{term "maximum A"};
    1.30 -if is_dsc t then () else error "is_dsc changed 2";
    1.31 +if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 2";
    1.32  
    1.33  val t = head_of @{term "fixedValues [R=(R::real)]"};
    1.34 -if is_dsc t then () else error "is_dsc changed 3";
    1.35 +if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 3";
    1.36