--- a/src/HOL/Hoare/Hoare.ML Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Hoare.ML Fri Mar 08 13:11:09 1996 +0100
@@ -10,19 +10,19 @@
(*** Hoare rules ***)
-val SkipRule = prove_goalw thy [SpecDef,SkipDef]
+val SkipRule = prove_goalw thy [Spec_def,Skip_def]
"(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
(fn prems => [fast_tac (HOL_cs addIs prems) 1]);
-val AssignRule = prove_goalw thy [SpecDef,AssignDef]
+val AssignRule = prove_goalw thy [Spec_def,Assign_def]
"(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
(fn prems => [fast_tac (HOL_cs addIs prems) 1]);
-val SeqRule = prove_goalw thy [SpecDef,SeqDef]
+val SeqRule = prove_goalw thy [Spec_def,Seq_def]
"[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
(fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
-val IfRule = prove_goalw thy [SpecDef,CondDef]
+val IfRule = prove_goalw thy [Spec_def,Cond_def]
"[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
\ Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
\ ==> Spec p (Cond b c c') r"
@@ -33,14 +33,14 @@
cut_facts_tac [prem2,prem3] 1,
fast_tac (HOL_cs addIs [prem1]) 1]);
-val strenthen_pre = prove_goalw thy [SpecDef]
+val strenthen_pre = prove_goalw thy [Spec_def]
"[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
(fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
fast_tac (HOL_cs addIs [prem1]) 1]);
-val [iter_0,iter_Suc] = nat_recs IterDef;
+val [iter_0,iter_Suc] = nat_recs Iter_def;
-val lemma = prove_goalw thy [SpecDef,WhileDef]
+val lemma = prove_goalw thy [Spec_def,While_def]
"[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
\ ==> Spec inv (While b inv c) q"
(fn [prem1,prem2] =>
@@ -49,7 +49,7 @@
res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
simp_tac (!simpset addsimps [iter_0]) 1,
fast_tac (HOL_cs addIs [prem2]) 1,
- simp_tac (!simpset addsimps [iter_Suc,SeqDef]) 1,
+ simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
val WhileRule = lemma RSN (2,strenthen_pre);