equal
deleted
inserted
replaced
|
1 (* use"tests/list_rls.sml"; |
|
2 W.N. 8.01 |
|
3 only one item per file for test-impl. |
|
4 *) |
|
5 |
|
6 |
|
7 val thy' = "ListG.thy"; |
|
8 val ct = "length_ [1,1,1]"; |
|
9 val thm = ("length_Cons_",""); |
|
10 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
|
11 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
|
12 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
|
13 val thm = ("length_Nil_",""); |
|
14 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
|
15 if ct="1 + (1 + (1 + 0))"then() |
|
16 else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct); |
|
17 |
|
18 |
|
19 val ct = "length_ [1,1,1]"; |
|
20 val rls = "list_rls"; |
|
21 val (ct,asm) = the (rewrite_set thy' false rls ct); |
|
22 if ct="3"then() |
|
23 else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct); |
|
24 |
|
25 |
|
26 val ct = "length_ [1,1,1]"; |
|
27 val t = (term_of o the o (parse ListG.thy)) ct; |
|
28 val t = eval_listexpr_ ListG.thy list_rls t; |
|
29 case t of Free ("3",_) => () |
|
30 | _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct); |
|
31 |
|
32 |