# HG changeset patch
# User wenzelm
# Date 1256854655 -3600
# Node ID c5cd93763e714785609541f7ac9d07f8f07010de
# Parent  0affc253597974a3754848e1f655b0d7e4c37e76
recovered from 7a1f597f454e, simplified imports;

diff -r 0affc2535979 -r c5cd93763e71 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Thu Oct 29 22:29:51 2009 +0100
+++ b/src/HOL/ex/Numeral.thy	Thu Oct 29 23:17:35 2009 +0100
@@ -5,7 +5,7 @@
 header {* An experimental alternative numeral representation. *}
 
 theory Numeral
-imports Plain Divides
+imports Main
 begin
 
 subsection {* The @{text num} type *}