src/HOL/UNITY/PPROD.ML

 
 
 (*** guarantees properties ***)
 
 Goalw [PLam_def]
-     "[| i : I;  lift_prog i (F i): X guar Y |] ==> (PLam I F) : X guar Y";
+    "[| i : I;  lift_prog i (F i): X guarantees Y |]  \
+\    ==> (PLam I F) : X guarantees Y";
 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
 qed "guarantees_PLam_I";
 
 Goalw [PLam_def]
-    "[| ALL i:I. F i : X guar Y |] \
+    "[| ALL i:I. F i : X guarantees Y |] \
 \    ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
-\                 guar (INT i: I. lift_prog i `` Y)";
+\                 guarantees (INT i: I. lift_prog i `` Y)";
 by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
 bind_thm ("guarantees_PLam_INT", ballI RS result());
 
 Goalw [PLam_def]
-    "[| ALL i:I. F i : X guar Y |] \
+    "[| ALL i:I. F i : X guarantees Y |] \
 \    ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
-\                 guar (UN i: I. lift_prog i `` Y)";
+\                 guarantees (UN i: I. lift_prog i `` Y)";
 by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
 bind_thm ("guarantees_PLam_UN", ballI RS result());