equal
deleted
inserted
replaced
1 (* ID: $Id$ *) |
|
2 (* EXTRACT from HOL/ex/Primes.thy*) |
1 (* EXTRACT from HOL/ex/Primes.thy*) |
3 |
2 |
4 (*Euclid's algorithm |
3 (*Euclid's algorithm |
5 This material now appears AFTER that of Forward.thy *) |
4 This material now appears AFTER that of Forward.thy *) |
6 theory Primes imports Main begin |
5 theory Primes imports Main begin |
8 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
7 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
9 "gcd m n = (if n=0 then m else gcd n (m mod n))" |
8 "gcd m n = (if n=0 then m else gcd n (m mod n))" |
10 |
9 |
11 |
10 |
12 ML "Pretty.margin_default := 64" |
11 ML "Pretty.margin_default := 64" |
13 ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*) |
12 declare [[thy_output_indent = 5]] (*that is, Doc/TutorialI/settings.ML*) |
14 |
13 |
15 |
14 |
16 text {*Now in Basic.thy! |
15 text {*Now in Basic.thy! |
17 @{thm[display]"dvd_def"} |
16 @{thm[display]"dvd_def"} |
18 \rulename{dvd_def} |
17 \rulename{dvd_def} |