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