diff -r 4d0545e93c0d -r c533bc92e882 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))";