Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
authorwenzelm
Sat, 24 Oct 2009 18:55:27 +0200
changeset 33089 4e33c819fced
parent 33088 757d7787b10c
child 33090 2f05a1feac21
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Product_Type.thy	Sat Oct 24 17:49:44 2009 +0200
+++ b/src/HOL/Product_Type.thy	Sat Oct 24 18:55:27 2009 +0200
@@ -6,7 +6,7 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Inductive
+imports Inductive Nat
 uses
   ("Tools/split_rule.ML")
   ("Tools/inductive_set.ML")
isabelle