| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 28 Sep 2010 09:06:56 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 38031 | 460c24a6a6ba |
| parent 37960 | ec20007095f2 |
| child 41943 | f33f6959948b |
| permissions | -rw-r--r-- |
1 (* testexamples for Root, radicals
2 *)
4 val thy = Root.thy;
6 val t = str2term "sqrt 1";
7 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
8 if term2str t' = "1" then () else error "root.sml: diff.behav. sqrt 1";
9 val t = str2term "sqrt -1";
10 val NONE = rewrite_set_ thy false Root_erls t;
12 val t = str2term "sqrt 0";
13 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
14 term2str t';
15 if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1";