| 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-- |
| neuper@37906 | 1 |
(* testexamples for Root, radicals |
| neuper@37906 | 2 |
*) |
| neuper@37906 | 3 |
|
| neuper@37906 | 4 |
val thy = Root.thy; |
| neuper@37906 | 5 |
|
| neuper@37906 | 6 |
val t = str2term "sqrt 1"; |
| neuper@37926 | 7 |
val SOME (t',_) = rewrite_set_ thy false Root_erls t; |
| neuper@38031 | 8 |
if term2str t' = "1" then () else error "root.sml: diff.behav. sqrt 1"; |
| neuper@37906 | 9 |
val t = str2term "sqrt -1"; |
| neuper@37926 | 10 |
val NONE = rewrite_set_ thy false Root_erls t; |
| neuper@37906 | 11 |
|
| neuper@37906 | 12 |
val t = str2term "sqrt 0"; |
| neuper@37926 | 13 |
val SOME (t',_) = rewrite_set_ thy false Root_erls t; |
| neuper@37906 | 14 |
term2str t'; |
| neuper@38031 | 15 |
if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1"; |