1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/systest/list_rls.sml	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,32 @@
     1.4 +(* use"tests/list_rls.sml";
     1.5 +   W.N. 8.01
     1.6 +   only one item per file for test-impl.
     1.7 +*)
     1.8 +
     1.9 +
    1.10 +val thy' = "ListG.thy";
    1.11 +val ct = "length_ [1,1,1]";
    1.12 +val thm = ("length_Cons_","");
    1.13 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.14 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.15 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.16 +val thm = ("length_Nil_","");
    1.17 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.18 +if ct="1 + (1 + (1 + 0))"then()
    1.19 +else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
    1.20 +
    1.21 +
    1.22 +val ct = "length_ [1,1,1]";
    1.23 +val rls = "list_rls";
    1.24 +val (ct,asm) = the (rewrite_set thy' false rls ct);
    1.25 +if ct="3"then()
    1.26 +else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
    1.27 +
    1.28 +
    1.29 +val ct = "length_ [1,1,1]";
    1.30 +val t = (term_of o the o (parse ListG.thy)) ct;
    1.31 +val t = eval_listexpr_ ListG.thy list_rls t;
    1.32 +case t of Free ("3",_) => () 
    1.33 +| _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
    1.34 +
    1.35 +