# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1319887026 -3600
# Node ID ae49c5e8868eeedc53e7ba6d34ffd6f9d2c4bd9e
# Parent  dfbd535cd1fdb096f309e9d410de664eb76a62fa
test

diff -r dfbd535cd1fd -r ae49c5e8868e ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Thu Oct 27 18:11:52 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Sat Oct 29 12:17:06 2011 +0100
@@ -662,14 +662,6 @@
   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
 *}
 
-ML {*
-  val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = 
-  @{context}
-  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
 
 text {*
   Recall that @{ML "|>"} is the reverse function application. Recall also that
diff -r dfbd535cd1fd -r ae49c5e8868e progtutorial.pdf
Binary file progtutorial.pdf has changed