| changeset 5620 | 3ac11c4af76a |
| parent 5608 | a82a038a3e7a |
| child 5640 | 4a59d99b5ca3 |
--- a/src/HOL/UNITY/WFair.ML Wed Oct 07 10:31:30 1998 +0200 +++ b/src/HOL/UNITY/WFair.ML Wed Oct 07 10:32:00 1998 +0200 @@ -434,7 +434,7 @@ \ constrains acts (A1 - B) (A1 Un B); \ \ constrains acts (A2 - C) (A2 Un C) |] \ \ ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)"; -by(Blast_tac 1); +by (Blast_tac 1); val lemma1 = result();