# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1236355936 0
# Node ID 83f36a1c62f29d561d18b3f813eb09a45f090c99
# Parent  cc9359bfacf411b4a8cd9be7d04fe2b285641128
rolled back the changes on the function warning and tracing

diff -r cc9359bfacf4 -r 83f36a1c62f2 CookBook/Base.thy
--- a/CookBook/Base.thy	Thu Mar 05 16:46:43 2009 +0000
+++ b/CookBook/Base.thy	Fri Mar 06 16:12:16 2009 +0000
@@ -14,10 +14,10 @@
     (OuterParse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 *}
-
+(*
 ML {*
   fun warning str = str
   fun tracing str = str
 *}
-
+*)
 end
diff -r cc9359bfacf4 -r 83f36a1c62f2 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Thu Mar 05 16:46:43 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Mar 06 16:12:16 2009 +0000
@@ -73,14 +73,14 @@
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
   the function @{ML "warning"}. For example 
 
-  @{ML_response [display,gray] "warning \"any string\"" "\"any string\""}
+  @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
 
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
   converting values into strings, namely the function @{ML makestring}:
 
-  @{ML_response [display,gray] "warning (makestring 1)" "\"1\""} 
+  @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
 
   However @{ML makestring} only works if the type of what is converted is monomorphic 
   and not a function.
@@ -91,7 +91,7 @@
   function @{ML tracing} is more appropriate. This function writes all output into
   a separate tracing buffer. For example:
 
-  @{ML_response [display,gray] "tracing \"foo\"" "\"foo\""}
+  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 
   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 
   printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 
@@ -708,6 +708,7 @@
   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
   | is_nil_or_all _ = false *}
 
+(*
 text {*
   Occasional you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
@@ -725,7 +726,7 @@
   FIXME: Find the right files to do with naming.
   \end{readmore}
 *}
-
+*)
 
 section {* Type-Checking *}
 
diff -r cc9359bfacf4 -r 83f36a1c62f2 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Thu Mar 05 16:46:43 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Mar 06 16:12:16 2009 +0000
@@ -2,6 +2,7 @@
 imports Base FirstSteps
 begin
 
+
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
diff -r cc9359bfacf4 -r 83f36a1c62f2 cookbook.pdf
Binary file cookbook.pdf has changed