changeset 65552 | f533820e7248 |
parent 64246 | 15d1ee6e847b |
child 66453 | cc19f7ca2ed6 |
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sat Apr 22 12:52:55 2017 +0200 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sat Apr 22 22:01:35 2017 +0200 @@ -4,7 +4,7 @@ *) theory Greatest_Common_Divisor -imports "../../SPARK" GCD +imports "../../SPARK" begin spark_proof_functions