src/HOL/UNITY/PPROD.ML
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7947 b999c1ab9327
     1.1 --- a/src/HOL/UNITY/PPROD.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/PPROD.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -6,10 +6,13 @@
     1.4  Abstraction over replicated components (PLam)
     1.5  General products of programs (Pi operation)
     1.6  
     1.7 -It is not clear that any of this is good for anything.
     1.8 +Probably some dead wood here!
     1.9  *)
    1.10  
    1.11  
    1.12 +val image_eqI' = read_instantiate_sg (sign_of thy)
    1.13 +                     [("x", "?ff(i := ?u)")] image_eqI;
    1.14 +
    1.15  (*** Basic properties ***)
    1.16  
    1.17  Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";