# HG changeset patch
# User paulson
# Date 864998256 -7200
# Node ID 51ed014406fa4790a11702debb66d4af7eed0dd9
# Parent  be517d000c02f157a25a0e0565a3686912ee0153
New theory Divides

diff -r be517d000c02 -r 51ed014406fa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 30 15:17:14 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri May 30 15:17:36 1997 +0200
@@ -10,7 +10,7 @@
 
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
-	Sexp Univ List RelPow Option
+	Divides Sexp Univ List RelPow Option
 
 PROVERS = hypsubst.ML classical.ML blast.ML \
 	simplifier.ML splitter.ML nat_transitive.ML