Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/root.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37960 ec20007095f2
child 41943 f33f6959948b
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba 
     3 
     3 
     4 val thy = Root.thy;
 
     4 val thy = Root.thy;
 
     5 
     5 
     6 val t = str2term "sqrt 1";
 
     6 val t = str2term "sqrt 1";
 
     7 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
 
     7 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
 
     8 if term2str t' = "1" then () else raise error "root.sml: diff.behav. sqrt 1";
 
     8 if term2str t' = "1" then () else error "root.sml: diff.behav. sqrt 1";
 
     9 val t = str2term "sqrt -1";
 
     9 val t = str2term "sqrt -1";
 
    10 val NONE = rewrite_set_ thy false Root_erls t;
 
    10 val NONE = rewrite_set_ thy false Root_erls t;
 
    11 
    11 
    12 val t = str2term "sqrt 0";
 
    12 val t = str2term "sqrt 0";
 
    13 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
 
    13 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
 
    14 term2str t';
 
    14 term2str t';
 
    15 if term2str t' = "0" then () else raise error "root.sml: diff.behav. sqrt 1";
 
    15 if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1";
wneuper/isa