diff -r 3a8d722fd3ff -r 16c4ea954511 IOA/example/Multiset.ML --- a/IOA/example/Multiset.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/IOA/example/Multiset.ML Mon Nov 21 17:50:34 1994 +0100 @@ -10,21 +10,21 @@ goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def] "count({|},x) = 0"; by (rtac refl 1); -val count_empty = result(); +qed "count_empty"; goal Multiset.thy "count(addm(M,x),y) = if(y=x,Suc(count(M,y)),count(M,y))"; by (asm_simp_tac (arith_ss addsimps [Multiset.count_def,Multiset.countm_nonempty_def] setloop (split_tac [expand_if])) 1); -val count_addm_simp = result(); +qed "count_addm_simp"; goal Multiset.thy "count(M,y) <= count(addm(M,x),y)"; by (simp_tac (arith_ss addsimps [count_addm_simp] setloop (split_tac [expand_if])) 1); by (rtac impI 1); by (rtac (le_refl RS (leq_suc RS mp)) 1); -val count_leq_addm = result(); +qed "count_leq_addm"; goalw Multiset.thy [Multiset.count_def] "count(delm(M,x),y) = if(y=x,pred(count(M,y)),count(M,y))"; @@ -38,7 +38,7 @@ setloop (split_tac [expand_if])) 1); by (safe_tac HOL_cs); by (asm_full_simp_tac HOL_ss 1); -val count_delm_simp = result(); +qed "count_delm_simp"; goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm(M,P) <= countm(M,Q))"; by (res_inst_tac [("M","M")] Multiset.induction 1); @@ -47,7 +47,7 @@ by (etac (less_eq_add_cong RS mp RS mp) 1); by (asm_full_simp_tac (arith_ss addsimps [le_eq_less_or_eq] setloop (split_tac [expand_if])) 1); -val countm_props = result(); +qed "countm_props"; goal Multiset.thy "!!P. ~P(obj) ==> countm(M,P) = countm(delm(M,obj),P)"; by (res_inst_tac [("M","M")] Multiset.induction 1); @@ -56,7 +56,7 @@ by (asm_simp_tac (arith_ss addsimps[Multiset.countm_nonempty_def, Multiset.delm_nonempty_def] setloop (split_tac [expand_if])) 1); -val countm_spurious_delm = result(); +qed "countm_spurious_delm"; goal Multiset.thy "!!P. P(x) ==> 0 0 0 countm(delm(M,x),P) = pred(countm(M,P))"; @@ -81,4 +81,4 @@ Multiset.countm_nonempty_def,pos_count_imp_pos_countm, suc_pred_id] setloop (split_tac [expand_if])) 1); -val countm_done_delm = result(); +qed "countm_done_delm";