1 (* Title: "Specify/input-descript.sml"
2 Author: Walther Neuper 060605
3 (c) due to copyright terms
5 "----------------------------------------------------------------------------------------------";
6 "table of contents ----------------------------------------------------------------------------";
7 "----------------------------------------------------------------------------------------------";
8 "-------- distinguish input to Model ----------------------------------------------------------";
9 "----------------------------------------------------------------------------------------------";
10 "----------------------------------------------------------------------------------------------";
11 "----------------------------------------------------------------------------------------------";
14 "-------- distinguish input to Model ----------------------------------------------------------";
15 "-------- distinguish input to Model ----------------------------------------------------------";
16 "-------- distinguish input to Model ----------------------------------------------------------";
17 "----- fun is_booll_dsc -----";
18 val t as Const ("Input_Descript.relations",
19 Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]),
20 Type ("Input_Descript.una", [])])) = @{term "relations"};
22 if is_booll_dsc t then () else error "is_booll_dsc changed";
23 "----- fun is_reall_dsc -----";
24 if not (is_reall_dsc t) then () else error "is_reall_dsc changed";
26 "----- fun is_list_dsc -----";
27 val t = @{term "someList"};
28 if is_list_dsc t then () else error "is_list_dsc changed 1";
30 val t = @{term "additionalRels [a=b,c=(d::real)]"};
31 if is_list_dsc t then () else error "is_list_dsc changed 2";
32 if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
34 "----- fun is_list_dsc -----";
35 val t = @{term "maximum"};
36 if is_dsc t then () else error "is_dsc changed 1";
38 val t = head_of @{term "maximum A"};
39 if is_dsc t then () else error "is_dsc changed 2";
41 val t = head_of @{term "fixedValues [R=(R::real)]"};
42 if is_dsc t then () else error "is_dsc changed 3";