src/HOL/UNITY/WFair.ML
changeset 9084 090d450af656
parent 8948 b797cfa3548d
child 10064 1a77667b21ef
equal deleted inserted replaced
9083:b36787a56a1f 9084:090d450af656
    39 by (rtac (major RS CollectD RS bexE) 1);
    39 by (rtac (major RS CollectD RS bexE) 1);
    40 by (blast_tac (claset() addIs prems) 1);
    40 by (blast_tac (claset() addIs prems) 1);
    41 qed "transientE";
    41 qed "transientE";
    42 
    42 
    43 Goalw [transient_def] "transient UNIV = {}";
    43 Goalw [transient_def] "transient UNIV = {}";
    44 by Auto_tac;
    44 by (Blast_tac 1); 
    45 qed "transient_UNIV";
    45 qed "transient_UNIV";
    46 
    46 
    47 Goalw [transient_def] "transient {} = UNIV";
    47 Goalw [transient_def] "transient {} = UNIV";
    48 by Auto_tac;
    48 by Auto_tac;
    49 qed "transient_empty";
    49 qed "transient_empty";