src/HOL/UNITY/Comp.thy
changeset 8055 bb15396278fb
parent 7399 cf780c2bcccf
child 8122 b43ad07660b9
     1.1 --- a/src/HOL/UNITY/Comp.thy	Wed Dec 08 13:52:36 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Wed Dec 08 13:53:29 1999 +0100
     1.3 @@ -19,4 +19,11 @@
     1.4  
     1.5    strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
     1.6  
     1.7 +constdefs
     1.8 +  preserves :: "('a=>'b) => 'a program set"
     1.9 +    "preserves v == INT z. stable {s. v s = z}"
    1.10 +
    1.11 +  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    1.12 +    "funPair f g == %x. (f x, g x)"
    1.13 +
    1.14  end