| changeset 61980 | 6b780867d426 |
| parent 60770 | 240563fbf41d |
| child 65449 | c82e63b11b8b |
--- a/src/ZF/UNITY/State.thy Wed Dec 30 17:38:57 2015 +0100 +++ b/src/ZF/UNITY/State.thy Wed Dec 30 17:45:18 2015 +0100 @@ -21,7 +21,7 @@ default_val :: "i=>i" definition - "state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))" + "state == \<Prod>x \<in> var. cons(default_val(x), type_of(x))" definition "st0 == \<lambda>x \<in> var. default_val(x)"