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.
plugged in pre-existing theories appropriately
authorhaftmann
Sat, 03 Mar 2012 22:38:53 +0100
changeset 46791 e1569a38448c
parent 46790 f3c10e908f65
child 46792 69b107201040
plugged in pre-existing theories appropriately
src/HOL/Import/HOL4/Generate.thy file | annotate | diff | comparison | revisions
src/HOL/Import/HOL4/Imported.thy file | annotate | diff | comparison | revisions
src/HOL/Import/HOL_Light/Generate.thy file | annotate | diff | comparison | revisions
src/HOL/Import/HOL_Light/Imported.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/HOL4/Generate.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL4/Generate.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,5 @@
 theory Generate
-imports Compatibility
+imports "Template/GenHOL4Prob" "Template/GenHOL4Vec" "Template/GenHOL4Word32"
 begin
 
 end
--- a/src/HOL/Import/HOL4/Imported.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL4/Imported.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,6 @@
 theory Imported
-imports Compatibility
+imports "Generated/HOL4Vec" "Generated/HOL4Word32" "Generated/HOL4Real" "Generated/HOL4Prob"
 begin
 
 end
+
--- a/src/HOL/Import/HOL_Light/Generate.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Generate.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,5 @@
 theory Generate
-imports Compatibility
+imports "Template/GenHOLLight"
 begin
 
 end
--- a/src/HOL/Import/HOL_Light/Imported.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Imported.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,6 @@
 theory Imported
-imports Compatibility
+imports "Generated/HOLLight"
 begin
 
 end
+
isabelle