(* use"tests/list_rls.sml";

    W.N. 8.01

    only one item per file for test-impl.

 *)

 val thy' = "ListG.thy";

 val ct = "length_ [1,1,1]";

 val thm = ("length_Cons_","");

 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

 val thm = ("length_Nil_","");

 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

 if ct="1 + (1 + (1 + 0))"then()

 else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);

 val ct = "length_ [1,1,1]";

 val rls = "list_rls";

 val (ct,asm) = the (rewrite_set thy' false rls ct);

 if ct="3"then()

 else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);

 val ct = "length_ [1,1,1]";

 val t = (term_of o the o (parse ListG.thy)) ct;

 val t = eval_listexpr_ ListG.thy list_rls t;

 case t of Free ("3",_) => () 

 | _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);