diff -r c495eb16beb6 -r cfd644dfc3b4 PIPBasics.thy --- a/PIPBasics.thy Wed Jan 27 19:28:42 2016 +0800 +++ b/PIPBasics.thy Wed Jan 27 23:34:23 2016 +0800 @@ -3784,4 +3784,5 @@ end + end