--- a/src/HOL/Isar_examples/Fibonacci.thy Mon Sep 04 10:25:32 2000 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Sep 04 10:26:34 2000 +0200
@@ -78,7 +78,7 @@
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)";
by simp;
also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))";
- by (simp only: gcd_add2);
+ by (simp only: gcd_add2');
also; have "... = gcd (fib (n + 1), fib (n + 1 + 1))";
by (simp add: gcd_commute);
also; assume "... = 1";
--- a/src/HOL/ex/Factorization.ML Mon Sep 04 10:25:32 2000 +0200
+++ b/src/HOL/ex/Factorization.ML Mon Sep 04 10:26:34 2000 +0200
@@ -6,6 +6,9 @@
Fundamental Theorem of Arithmetic (unique factorization into primes)
*)
+val prime_def = thm "prime_def";
+val prime_dvd_mult = thm "prime_dvd_mult";
+
(* --- Arithmetic --- *)
--- a/src/HOL/ex/Fib.ML Mon Sep 04 10:25:32 2000 +0200
+++ b/src/HOL/ex/Fib.ML Mon Sep 04 10:26:34 2000 +0200
@@ -64,9 +64,16 @@
(** Towards Law 6.111 of Concrete Mathematics **)
+val gcd_induct = thm "gcd_induct";
+val gcd_commute = thm "gcd_commute";
+val gcd_add2 = thm "gcd_add2";
+val gcd_non_0 = thm "gcd_non_0";
+val gcd_mult_cancel = thm "gcd_mult_cancel";
+
+
Goal "gcd(fib n, fib (Suc n)) = 1";
by (induct_thm_tac fib.induct "n" 1);
-by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
+by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3);
by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
qed "gcd_fib_Suc_eq_1";