diff -r 29800666e526 -r 842917225d56 src/HOL/ex/Pythagoras.thy --- a/src/HOL/ex/Pythagoras.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/ex/Pythagoras.thy Tue Feb 23 16:25:08 2016 +0100 @@ -29,4 +29,4 @@ shows "vecsqnorm(vector C A) = vecsqnorm(vector B A) + vecsqnorm(vector C B)" using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv) - end \ No newline at end of file + end