--- a/CookBook/FirstSteps.thy	Thu Oct 30 13:36:51 2008 +0100
+++ b/CookBook/FirstSteps.thy	Sat Nov 01 15:20:36 2008 +0100
@@ -329,8 +329,6 @@
 
 section {* Type Checking *}
 
-ML {* cterm_of @{theory} @{term "a + b = c"} *}
-
 text {* 
   
   We can freely construct and manipulate terms, since they are just
@@ -409,7 +407,7 @@
   Qt 
   |> implies_intr assm2
   |> implies_intr assm1
-end" "(FIXME)"}
+end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 
   This code-snippet constructs the following proof:
 
@@ -489,7 +487,6 @@
 apply assumption
 done
 
-
 text {*
   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets 
   up a goal state for proving the goal @{text C} under the assumptions @{text As} 
@@ -509,7 +506,7 @@
     THEN assume_tac 1
     THEN resolve_tac [disjI1] 1
     THEN assume_tac 1)
-end" "(FIXME)"}
+end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
   \begin{readmore}
   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
@@ -529,7 +526,7 @@
     THEN' assume_tac 
     THEN' resolve_tac [disjI1] 
     THEN' assume_tac) 1)
-end" "(FIXME)"}
+end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
   (FIXME: are there any advantages/disadvantages about this way?) 
 *}