made definition more readable
authorpaulson
Fri May 21 10:58:47 1999 +0200 (1999-05-21)
changeset 6677629b4b3d5bee
parent 6676 62d1e642da30
child 6678 d83f27b03529
made definition more readable
src/HOL/UNITY/Extend.thy
     1.1 --- a/src/HOL/UNITY/Extend.thy	Fri May 21 10:56:46 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Fri May 21 10:58:47 1999 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4      "extend_set h A == h `` (A Times UNIV)"
     1.5  
     1.6    extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c * 'c) set"
     1.7 -    "extend_act h == (%act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))})"
     1.8 +    "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
     1.9  
    1.10    extend :: "['a*'b => 'c, 'a program] => 'c program"
    1.11      "extend h F == mk_program (extend_set h (Init F),