changeset 66453 | cc19f7ca2ed6 |
parent 53015 | a1119cf551e8 |
child 67019 | 7a3724078363 |
--- a/src/HOL/IMP/Live_True.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/IMP/Live_True.thy Fri Aug 18 20:47:47 2017 +0200 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Live_True -imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step +imports "HOL-Library.While_Combinator" Vars Big_Step begin subsection "True Liveness Analysis"