equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 theory Atools imports Descript Script |
6 theory Atools imports Descript Script |
7 begin |
7 begin |
8 |
8 |
|
9 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z" |
|
10 where "auto_generated t_t = t_t" |
|
11 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z" |
|
12 where "auto_generated_inst t_t v = t_t" |
9 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml" |
13 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml" |
10 |
14 |
11 consts |
15 consts |
12 |
16 |
13 Arbfix :: "real" |
17 Arbfix :: "real" |