changeset 10265 | 4e004b548049 |
parent 9019 | 9c1118619d6c |
child 13796 | 19f50fa807ae |
--- a/src/HOL/UNITY/Follows.thy Wed Oct 18 23:41:28 2000 +0200 +++ b/src/HOL/UNITY/Follows.thy Wed Oct 18 23:42:18 2000 +0200 @@ -4,11 +4,9 @@ Copyright 1998 University of Cambridge The "Follows" relation of Charpentier and Sivilotte - -add_path "../Induct"; *) -Follows = SubstAx + ListOrder + MultisetOrder + +Follows = SubstAx + ListOrder + Multiset + constdefs