Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nat.thy
changeset 35121 36c0a6dd8c6f
parent 35064 1bdef0c013d3
child 35216 7641e8d831d2 
--- a/src/HOL/Nat.thy	Fri Feb 12 09:49:28 2010 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 12 14:28:01 2010 +0100
@@ -8,7 +8,7 @@
 header {* Natural numbers *}
 
 theory Nat
-imports Inductive Product_Type Fields
+imports Inductive Typedef Fun Fields
 uses
   "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"
isabelle