# HG changeset patch
# User paulson
# Date 968055994 -7200
# Node ID 5b5d9ee742ca70930886803d3502fef967ff47ad
# Parent  a0fcf6f0436c1d2f79e455f59e8cb44113f442f7
minor fixes for new version of Primes.thy

diff -r a0fcf6f0436c -r 5b5d9ee742ca src/HOL/Isar_examples/Fibonacci.thy
--- 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";
diff -r a0fcf6f0436c -r 5b5d9ee742ca src/HOL/ex/Factorization.ML
--- 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 --- *)
 
diff -r a0fcf6f0436c -r 5b5d9ee742ca src/HOL/ex/Fib.ML
--- 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";