--- a/ProgTutorial/Parsing.thy	Wed Apr 07 11:32:00 2010 +0200
+++ b/ProgTutorial/Parsing.thy	Sat Apr 24 22:55:50 2010 +0200
@@ -15,6 +15,13 @@
 chapter {* Parsing\label{chp:parsing} *}
 
 text {*
+  \begin{flushright}
+  {\em An important principle underlying the success and popularity of Unix\\ is
+  the philosophy of building on the work of others.} \\[1ex]
+  Linus Torwalds in the email exchange\\ with Andrew S.~Tannenbaum
+  \end{flushright}
+
+
   Isabelle distinguishes between \emph{outer} and \emph{inner}
   syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}
   and so on, belong to the outer syntax, whereas terms, types and so on belong
@@ -1386,6 +1393,37 @@
   \end{minipage} *}
 (*<*)oops(*>*)
 
+method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
+
+lemma "True"
+apply(test)
+oops
+
+method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
+
+lemma "False"
+apply(joker)
+oops
+
+text {* if true is set then always works *}
+
+ML {* atac *} 
+
+method_setup first_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD (atac 1)))) *} {* bla *}
+
+ML {* HEADGOAL *}
+
+lemma "A \<Longrightarrow> A"
+apply(first_atac)
+oops
+
+method_setup my_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD' atac))) *} {* bla *}
+
+lemma "A \<Longrightarrow> A"
+apply(my_atac)
+oops
+
+
 
 
 
@@ -1398,7 +1436,23 @@
 ML {* Scan.succeed  *}
 *)
 
+ML {* resolve_tac *}
+
+method_setup myrule =
+  {* Scan.lift (Scan.succeed (K (METHOD (fn thms => resolve_tac thms 1)))) *}
+  {* bla *}
+
+lemma
+  assumes a: "A \<Longrightarrow> B \<Longrightarrow> C"
+  shows "C"
+using a
+apply(myrule)
+oops
+
+
+
 text {*
+  (********************************************************)
   (FIXME: explain a version of rule-tac)
 *}