src/HOL/UNITY/UNITY.ML
changeset 5340 d75c03cf77b5
parent 5313 1861a564d7e2
child 5608 a82a038a3e7a
     1.1 --- a/src/HOL/UNITY/UNITY.ML	Wed Aug 19 10:29:01 1998 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY.ML	Wed Aug 19 10:34:31 1998 +0200
     1.3 @@ -14,6 +14,14 @@
     1.4  
     1.5  (*** constrains ***)
     1.6  
     1.7 +(*Map the type (anything => ('a set => anything) to just 'a*)
     1.8 +fun overload_2nd_set s =
     1.9 +    Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type);
    1.10 +
    1.11 +overload_2nd_set "UNITY.constrains";
    1.12 +overload_2nd_set "UNITY.stable";
    1.13 +overload_2nd_set "UNITY.unless";
    1.14 +
    1.15  val prems = Goalw [constrains_def]
    1.16      "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
    1.17  \    ==> constrains acts A A'";