ex/SList.ML

--- a/ex/SList.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/SList.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -30,7 +30,7 @@
 qed "list_sexp";
 
 (* A <= sexp ==> list(A) <= sexp *)
-val list_subset_sexp = standard ([list_mono, list_sexp] MRS subset_trans);
+bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
 
 (*Induction for the type 'a list *)
 val prems = goalw SList.thy [Nil_def,Cons_def]
@@ -64,9 +64,9 @@
 goalw SList.thy list_con_defs "CONS(M,N) ~= NIL";
 by (rtac In1_not_In0 1);
 qed "CONS_not_NIL";
-val NIL_not_CONS = standard (CONS_not_NIL RS not_sym);
+bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
 
-val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
+bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
 val NIL_neq_CONS = sym RS CONS_neq_NIL;
 
 goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
@@ -74,9 +74,9 @@
 by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
 qed "Cons_not_Nil";
 
-val Nil_not_Cons = standard (Cons_not_Nil RS not_sym);
+bind_thm ("Nil_not_Cons", (Cons_not_Nil RS not_sym));
 
-val Cons_neq_Nil = standard (Cons_not_Nil RS notE);
+bind_thm ("Cons_neq_Nil", (Cons_not_Nil RS notE));
 val Nil_neq_Cons = sym RS Cons_neq_Nil;
 
 (** Injectiveness of CONS and Cons **)
@@ -85,7 +85,7 @@
 by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
 qed "CONS_CONS_eq";
 
-val CONS_inject = standard (CONS_CONS_eq RS iffD1 RS conjE);
+bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
 
 (*For reasoning about abstract list constructors*)
 val list_cs = set_cs addIs [Rep_list] @ list.intrs
@@ -96,7 +96,7 @@
 goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
 by (fast_tac list_cs 1);
 qed "Cons_Cons_eq";
-val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE);
+bind_thm ("Cons_inject", (Cons_Cons_eq RS iffD1 RS conjE));
 
 val [major] = goal SList.thy "CONS(M,N): list(A) ==> M: A & N: list(A)";
 by (rtac (major RS setup_induction) 1);