Mercurial Mercurial > hg > isabelle-cookbook / 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.
Antiquotation setup is now contained in theory Base.
authorberghofe
Fri, 10 Oct 2008 17:06:26 +0200
changeset 25 e2f9f94b26d4
parent 24 9d5d2f9d7c09
child 26 2311f81d7a22
Antiquotation setup is now contained in theory Base.
CookBook/FirstSteps.thy file | annotate | diff | comparison | revisions
CookBook/Recipes/NamedThms.thy file | annotate | diff | comparison | revisions
CookBook/Solutions.thy file | annotate | diff | comparison | revisions 
--- a/CookBook/FirstSteps.thy	Fri Oct 10 17:04:05 2008 +0200
+++ b/CookBook/FirstSteps.thy	Fri Oct 10 17:06:26 2008 +0200
@@ -1,7 +1,5 @@
 theory FirstSteps
-imports Main
-uses "antiquote_setup.ML"
-     "antiquote_setup_plus.ML"
+imports Base
 begin
 
 
--- a/CookBook/Recipes/NamedThms.thy	Fri Oct 10 17:04:05 2008 +0200
+++ b/CookBook/Recipes/NamedThms.thy	Fri Oct 10 17:06:26 2008 +0200
@@ -1,8 +1,5 @@
-
 theory NamedThms
-imports Main
-uses "antiquote_setup.ML"
-     "antiquote_setup_plus.ML"
+imports Base
 begin
 
 section {* Accumulate a List of Theorems under a Name *} 
--- a/CookBook/Solutions.thy	Fri Oct 10 17:04:05 2008 +0200
+++ b/CookBook/Solutions.thy	Fri Oct 10 17:06:26 2008 +0200
@@ -1,7 +1,5 @@
 theory Solutions
-imports Main
-uses "antiquote_setup.ML"
-     "antiquote_setup_plus.ML"
+imports Base
 begin
 
 chapter {* Solutions to Most Exercises *}
isabelle-cookbook