10 Define specific constants for tacticals, which determine the flow of evaluation in programs. |
10 Define specific constants for tacticals, which determine the flow of evaluation in programs. |
11 Tacticals are not visible in calculations, which are generated by programs as a side effect. |
11 Tacticals are not visible in calculations, which are generated by programs as a side effect. |
12 \<close> |
12 \<close> |
13 subsection \<open>Consts for tacticals\<close> |
13 subsection \<open>Consts for tacticals\<close> |
14 consts |
14 consts |
15 Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10) (*@ used*) |
15 Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10) |
16 Try :: "['a => 'a, 'a] => 'a" |
16 Try :: "['a => 'a, 'a] => 'a" |
17 Repeat :: "['a => 'a, 'a] => 'a" |
17 Repeat :: "['a => 'a, 'a] => 'a" |
18 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10) |
18 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10) |
19 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9) |
19 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9) |
20 If :: "[bool, 'a, 'a] => 'a" ("(If (_)/ Then (_)/ Else (_))" 10) |
20 If :: "[bool, 'a, 'a] => 'a" ("(If (_)/ Then (_)/ Else (_))" 10) |