# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1305654413 -7200
# Node ID 21b5d0145fe4d64e204aaabab443e55585353d5c
# Parent  b6fc4d1b75d0bffe0ed27ae570edf1d6278b515a
updated to new Isabelle

diff -r b6fc4d1b75d0 -r 21b5d0145fe4 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Tue May 17 19:25:33 2011 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue May 17 19:46:53 2011 +0200
@@ -197,7 +197,7 @@
 
 ML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1
-    THEN auto_tac (clasimpset_of ctxt)*}
+    THEN auto_tac ctxt*}
 
 ML {*
   val conf = Function_Common.default_config
diff -r b6fc4d1b75d0 -r 21b5d0145fe4 progtutorial.pdf
Binary file progtutorial.pdf has changed