1 (* Title: Knowledge/root.sml
3 (c) due to copyright terms
5 "--------------------------------------------------------";
6 "table of contents --------------------------------------";
7 "--------------------------------------------------------";
8 "----------- rls Root_erls ------------------------------";
9 "--------------------------------------------------------";
10 "--------------------------------------------------------";
12 val thy = @{theory "Root"};
13 val ctxt = Proof_Context.init_global thy;
15 "----------- rls Root_erls ------------------------------";
16 "----------- rls Root_erls ------------------------------";
17 "----------- rls Root_erls ------------------------------";
18 val t = TermC.parse_test @{context} "sqrt 1";
19 val SOME (t',_) = rewrite_set_ ctxt false Root_erls t;
20 if UnparseC.term t' = "1" then () else error "root.sml: diff.behav. sqrt 1";
22 val t = TermC.parse_test @{context} "sqrt (- 1)";
23 val NONE = rewrite_set_ ctxt false Root_erls t;
25 val t = TermC.parse_test @{context} "sqrt 0";
26 val SOME (t',_) = rewrite_set_ ctxt false Root_erls t;
27 if UnparseC.term t' = "0" then () else error "root.sml: diff.behav. sqrt 1";