changeset 66453 | cc19f7ca2ed6 |
parent 53015 | a1119cf551e8 |
child 67019 | 7a3724078363 |
66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Live_True |
3 theory Live_True |
4 imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step |
4 imports "HOL-Library.While_Combinator" Vars Big_Step |
5 begin |
5 begin |
6 |
6 |
7 subsection "True Liveness Analysis" |
7 subsection "True Liveness Analysis" |
8 |
8 |
9 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |
9 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |