equal
deleted
inserted
replaced
3 author: Walther Neuper, Aug.2019 |
3 author: Walther Neuper, Aug.2019 |
4 (c) copyright due to lincense terms. |
4 (c) copyright due to lincense terms. |
5 *) |
5 *) |
6 |
6 |
7 theory Prog_Expr |
7 theory Prog_Expr |
8 imports Calculate ListC Program |
8 imports Calc_Binop ListC Program |
9 begin |
9 begin |
10 |
10 |
11 text \<open>Abstract: |
11 text \<open>Abstract: |
12 Specific constants are defined for pre-conditions of programs and for program-expressions. |
12 Specific constants are defined for pre-conditions of programs and for program-expressions. |
13 The constants are connected with ML functions for evaluation of respective expressions |
13 The constants are connected with ML functions for evaluation of respective expressions |