| changeset 66453 | cc19f7ca2ed6 |
| parent 64246 | 15d1ee6e847b |
| child 68407 | fd61a2e4e1f9 |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Example_Verification |
2 theory Example_Verification |
3 imports "../Examples/Gcd/Greatest_Common_Divisor" Simple_Greatest_Common_Divisor |
3 imports "HOL-SPARK-Examples.Greatest_Common_Divisor" Simple_Greatest_Common_Divisor |
4 begin |
4 begin |
5 (*>*) |
5 (*>*) |
6 |
6 |
7 chapter \<open>Verifying an Example Program\<close> |
7 chapter \<open>Verifying an Example Program\<close> |
8 |
8 |