| changeset 8072 | 5b95377d7538 |
| parent 8055 | bb15396278fb |
| child 8122 | b43ad07660b9 |
--- a/src/HOL/UNITY/ELT.thy Wed Dec 22 16:13:29 1999 +0100 +++ b/src/HOL/UNITY/ELT.thy Wed Dec 22 17:16:23 1999 +0100 @@ -17,7 +17,7 @@ inductive "elt CC F" intrs - Basis "[| F : A ensures B; A-B : CC |] ==> (A,B) : elt CC F" + Basis "[| F : A ensures B; A-B : (insert {} CC) |] ==> (A,B) : elt CC F" Trans "[| (A,B) : elt CC F; (B,C) : elt CC F |] ==> (A,C) : elt CC F"