src/HOL/UNITY/WFair.ML
changeset 7826 c6a8b73b6c2a
parent 7594 8a188ef6545e
child 7963 e7beff82e1ba
     1.1 --- a/src/HOL/UNITY/WFair.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/WFair.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -31,6 +31,15 @@
     1.4  by (Blast_tac 1);
     1.5  qed "transient_mem";
     1.6  
     1.7 +Goalw [transient_def] "transient UNIV = {}";
     1.8 +by Auto_tac;
     1.9 +qed "transient_UNIV";
    1.10 +
    1.11 +Goalw [transient_def] "transient {} = UNIV";
    1.12 +by Auto_tac;
    1.13 +qed "transient_empty";
    1.14 +Addsimps [transient_UNIV, transient_empty];
    1.15 +
    1.16  
    1.17  (*** ensures ***)
    1.18