
diff -r b11653b11bd3 -r cd612b489504 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Mon Oct 20 06:22:11 2008 +0000
+++ b/CookBook/FirstSteps.thy	Mon Oct 27 18:48:52 2008 +0100
@@ -5,7 +5,8 @@
 
 chapter {* First Steps *}
 
-text {* 
+text {*
+
   Isabelle programming is done in Standard ML.
   Just like lemmas and proofs, code in Isabelle is part of a 
   theory. If you want to follow the code written in this chapter, we 
@@ -27,11 +28,11 @@
   The easiest and quickest way to include code in a theory is
   by using the \isacommand{ML} command. For example\smallskip
 
-\isacommand{ML}
-@{ML_text "{"}@{ML_text "*"}\isanewline
+\isa{\isacommand{ML}
+\isacharverbatimopen\isanewline
 \hspace{5mm}@{ML "3 + 4"}\isanewline
-@{ML_text "*"}@{ML_text "}"}\isanewline
-@{ML_text "> 7"}\smallskip
+\isacharverbatimclose\isanewline
+@{ML_text "> 7"}\smallskip}
 
   Expressions inside \isacommand{ML} commands are immediately evaluated,
   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
@@ -40,15 +41,15 @@
   commands the undo operation behaves slightly counter-intuitive, because 
   if you define\smallskip
  
-\isacommand{ML}
-@{ML_text "{"}@{ML_text "*"}\isanewline
-@{ML_text "val foo = true"}\isanewline
-@{ML_text "*"}@{ML_text "}"}\isanewline
-@{ML_text "> true"}\smallskip
+\isa{\isacommand{ML}
+\isacharverbatimopen\isanewline
+\hspace{5mm}@{ML_text "val foo = true"}\isanewline
+\isacharverbatimclose\isanewline
+@{ML_text "> true"}\smallskip}
 
   then Isabelle's undo operation has no effect on the definition of 
   @{ML_text "foo"}. Note that from now on we will drop the 
-  \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever
+  \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
   we show code and its response.
 
   Once a portion of code is relatively stable, one usually wants to 
@@ -65,7 +66,8 @@
   \end{tabular}
   \end{center}
 
-  Note that from now on we are going to drop the the  
+  Note that from now on we are going to drop the 
+  \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}. 
   
 *}
 
@@ -100,25 +102,22 @@
   It is also possible to redirect the channel where the @{ML_text "foo"} is 
   printed to a separate file, e.g. to prevent Proof General from choking on massive 
   amounts of trace output. This rediretion can be achieved using the code
-*}
-
-ML {*
-  val strip_specials =
-  let
-    fun strip ("\^A" :: _ :: cs) = strip cs
-      | strip (c :: cs) = c :: strip cs
-      | strip [] = [];
-  in implode o strip o explode end;
 
-  fun redirect_tracing stream =
-  Output.tracing_fn := (fn s =>
+@{ML_decl [display]
+"val strip_specials =
+let
+  fun strip (\"\\^A\" :: _ :: cs) = strip cs
+    | strip (c :: cs) = c :: strip cs
+    | strip [] = [];
+in implode o strip o explode end;
+
+fun redirect_tracing stream =
+ Output.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
-     TextIO.output (stream, "\n");
-     TextIO.flushOut stream));
-*}
+     TextIO.output (stream, \"\\n\");
+     TextIO.flushOut stream));"}
 
-text {* 
-  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
+  Calling @{ML_text "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
 *}
@@ -143,13 +142,9 @@
   Note, however, that antiquotations are statically scoped, that is the value is
   determined at ``compile-time'', not ``run-time''. For example the function
 
-*}
+  @{ML_decl [display]
+  "fun not_current_thyname () = Context.theory_name @{theory}"}
 
-ML {* 
-  fun not_current_thyname () = Context.theory_name @{theory}
-*}
-
-text {*
   does \emph{not} return the name of the current theory, if it is run in a 
   different theory. Instead, the code above defines the constant function 
   that always returns the string @{ML_text "FirstSteps"}, no matter where the
@@ -160,7 +155,6 @@
 
   In a similar way you can use antiquotations to refer to theorems or simpsets:
 
-
   @{ML [display] "@{thm allI}"}
   @{ML [display] "@{simpset}"}
 
@@ -240,7 +234,7 @@
 
 text {*
 
-  @{ML_response [display] "@{typ \"bool \<Rightarrow> nat\"}" "Type \<dots>"}
+  @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
   (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
   internal representation. Is there a reason for this, that needs to be explained 
@@ -263,29 +257,19 @@
   dynamically. For example, a function that returns the implication 
   @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
   as arguments can only be written as
-*}
 
-
-ML {*
-  fun make_imp P Q tau =
+@{ML_decl [display]
+"fun make_imp P Q tau =
   let
-    val x = Free ("x",tau)
+    val x = Free (\"x\",tau)
   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
                                     HOLogic.mk_Trueprop (Q $ x)))
-  end
-*}
-
-text {*
+  end"}
 
   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
   @{term "tau"} into an antiquotation. For example the following does not work.
-*}
 
-ML {*
-  fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
-*}
-
-text {*
+  @{ML_decl [display] "fun make_wrong_imp P Q tau = @{prop \"\<And>x. P x \<Longrightarrow> Q x\"}"} 
 
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
   to both functions. 
@@ -397,18 +381,16 @@
   application. This combinator, and several variants are defined in
   @{ML_file "Pure/General/basics.ML"}.}
 
-*}
-
-ML {*
-let
+@{ML_response_fake [display]
+"let
   val thy = @{theory}
 
-  val assm1 = cterm_of thy @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
-  val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>bool) t)"}
+  val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
+  val assm2 = cterm_of thy @{prop \"((P::nat\<Rightarrow>bool) t)\"}
 
   val Pt_implies_Qt = 
         assume assm1
-        |> forall_elim (cterm_of thy @{term "t::nat"});
+        |> forall_elim (cterm_of thy @{term \"t::nat\"});
   
   val Qt = implies_elim Pt_implies_Qt (assume assm2);
 in
@@ -416,10 +398,7 @@
   Qt 
   |> implies_intr assm2
   |> implies_intr assm1
-end
-*}
-
-text {*
+end" "(FIXME)"}
 
   This code-snippet constructs the following proof:
 
@@ -507,51 +486,43 @@
   with the variables @{text xs} that will be generalised once the
   goal is proved. The @{text "tac"} is the tactic which proves the goal and which 
   can make use of the local assumptions.
-*}
 
-
-
-ML {*
-let
+@{ML_response_fake [display]
+"let
   val ctxt = @{context}
-  val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
+  val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
 in
-  Goal.prove ctxt ["P", "Q"] [] goal (fn _ => 
+  Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => 
     eresolve_tac [disjE] 1
     THEN resolve_tac [disjI2] 1
     THEN assume_tac 1
     THEN resolve_tac [disjI1] 1
     THEN assume_tac 1)
-end
-*}
-
-text {*
+end" "(FIXME)"}
 
   \begin{readmore}
   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
   \end{readmore}
 
-*}
 
-
-text {* An alternative way to transcribe this proof is as follows *}
+  An alternative way to transcribe this proof is as follows 
 
-ML {*
-let
+@{ML_response_fake [display]
+"let
   val ctxt = @{context}
-  val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
+  val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
 in
-  Goal.prove ctxt ["P", "Q"] [] goal (fn _ => 
+  Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => 
     (eresolve_tac [disjE] 
     THEN' resolve_tac [disjI2] 
     THEN' assume_tac 
     THEN' resolve_tac [disjI1] 
     THEN' assume_tac) 1)
-end
+end" "(FIXME)"}
+
+  (FIXME: are there any advantages/disadvantages about this way?) 
 *}
 
-text {* (FIXME: are there any advantages/disadvantages about this way?) *}
-
 section {* Storing Theorems *}
 
 section {* Theorem Attributes *}




