ex/LList.ML

--- a/ex/LList.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/LList.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -321,7 +321,7 @@
 qed "Lconst_fun_mono";
 
 (* Lconst(M) = CONS(M,Lconst(M)) *)
-val Lconst = standard (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski));
+bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski)));
 
 (*A typical use of co-induction to show membership in the gfp.
   The containing set is simply the singleton {Lconst(M)}. *)
@@ -365,9 +365,9 @@
 by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
 qed "LCons_not_LNil";
 
-val LNil_not_LCons = standard (LCons_not_LNil RS not_sym);
+bind_thm ("LNil_not_LCons", (LCons_not_LNil RS not_sym));
 
-val LCons_neq_LNil = standard (LCons_not_LNil RS notE);
+bind_thm ("LCons_neq_LNil", (LCons_not_LNil RS notE));
 val LNil_neq_LCons = sym RS LCons_neq_LNil;
 
 (** llist constructors **)
@@ -389,7 +389,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 llist constructors*)
@@ -401,7 +401,7 @@
 goalw LList.thy [LCons_def] "(LCons(x,xs)=LCons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac llist_cs 1);
 qed "LCons_LCons_eq";
-val LCons_inject = standard (LCons_LCons_eq RS iffD1 RS conjE);
+bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
 
 val [major] = goal LList.thy "CONS(M,N): llist(A) ==> M: A & N: llist(A)";
 by (rtac (major RS llist.elim) 1);
@@ -537,7 +537,7 @@
 by (ALLGOALS
     (asm_simp_tac Lappend_ss THEN'
      fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
-val Lappend_type = result();
+qed "Lappend_type";
 
 (*strong co-induction: bisimulation and case analysis on one variable*)
 goal LList.thy
@@ -863,7 +863,7 @@
 by (rtac (refl RS Pair_cong) 1);
 by (stac lmap_LNil 1);
 by (rtac refl 1);
-val lmap_lappend_distrib = result();
+qed "lmap_lappend_distrib";
 
 (*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
 goal LList.thy "lmap(f, lappend(l,n)) = lappend(lmap(f,l), lmap(f,n))";