# HG changeset patch
# User berghofe
# Date 1223651186 -7200
# Node ID e2f9f94b26d4f3e3a36348606faea0f32a8d83a7
# Parent  9d5d2f9d7c090a977cefefa3e16f66d6af887288
Antiquotation setup is now contained in theory Base.

diff -r 9d5d2f9d7c09 -r e2f9f94b26d4 CookBook/FirstSteps.thy
--- 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
 
 
diff -r 9d5d2f9d7c09 -r e2f9f94b26d4 CookBook/Recipes/NamedThms.thy
--- 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 *} 
diff -r 9d5d2f9d7c09 -r e2f9f94b26d4 CookBook/Solutions.thy
--- 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 *}