equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Rename.thy |
1 (* Title: HOL/UNITY/Rename.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 2000 University of Cambridge |
3 Copyright 2000 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header{*Renaming of State Sets*} |
6 section{*Renaming of State Sets*} |
7 |
7 |
8 theory Rename imports Extend begin |
8 theory Rename imports Extend begin |
9 |
9 |
10 definition rename :: "['a => 'b, 'a program] => 'b program" where |
10 definition rename :: "['a => 'b, 'a program] => 'b program" where |
11 "rename h == extend (%(x,u::unit). h x)" |
11 "rename h == extend (%(x,u::unit). h x)" |