author | paulson |
Fri, 21 May 1999 10:58:47 +0200 | |
changeset 6677 | 629b4b3d5bee |
parent 6676 | 62d1e642da30 |
child 6678 | d83f27b03529 |
--- a/src/HOL/UNITY/Extend.thy Fri May 21 10:56:46 1999 +0200 +++ b/src/HOL/UNITY/Extend.thy Fri May 21 10:58:47 1999 +0200 @@ -16,7 +16,7 @@ "extend_set h A == h `` (A Times UNIV)" extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c * 'c) set" - "extend_act h == (%act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))})" + "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}" extend :: "['a*'b => 'c, 'a program] => 'c program" "extend h F == mk_program (extend_set h (Init F),