equal
deleted
inserted
replaced
8 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
8 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
9 "gcd m n = (if n=0 then m else gcd n (m mod n))" |
9 "gcd m n = (if n=0 then m else gcd n (m mod n))" |
10 |
10 |
11 |
11 |
12 ML "Pretty.margin_default := 64" |
12 ML "Pretty.margin_default := 64" |
13 ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*) |
13 ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*) |
14 |
14 |
15 |
15 |
16 text {*Now in Basic.thy! |
16 text {*Now in Basic.thy! |
17 @{thm[display]"dvd_def"} |
17 @{thm[display]"dvd_def"} |
18 \rulename{dvd_def} |
18 \rulename{dvd_def} |