src/HOL/UNITY/UNITY.ML
changeset 7403 c318acb88251
parent 7345 59bc887290df
child 7594 8a188ef6545e
     1.1 --- a/src/HOL/UNITY/UNITY.ML	Wed Sep 01 11:15:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY.ML	Wed Sep 01 11:16:02 1999 +0200
     1.3 @@ -112,7 +112,9 @@
     1.4  
     1.5  (*** co ***)
     1.6  
     1.7 -overload_1st_set "UNITY.op co";
     1.8 +(*These operators are not overloaded, but their operands are sets, and 
     1.9 +  ultimately there's a risk of reaching equality, which IS overloaded*)
    1.10 +overload_1st_set "UNITY.constrains";
    1.11  overload_1st_set "UNITY.stable";
    1.12  overload_1st_set "UNITY.unless";
    1.13