# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1280346762 -3600
# Node ID 07be4fccd329f068d2d258a0feb5cb73554569c1
# Parent  7e33ba6190de8a009e39437d55b3b58538960513# Parent  520127b708e6f86a2d02400c1ab98f0a10836c6c
merged

diff -r 520127b708e6 -r 07be4fccd329 ProgTutorial/Package/Simple_Inductive_Package.thy
--- a/ProgTutorial/Package/Simple_Inductive_Package.thy	Wed Jul 28 19:09:49 2010 +0200
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy	Wed Jul 28 20:52:42 2010 +0100
@@ -54,7 +54,6 @@
 thm rel.accpart'.induct
 *)
 
-use "simple_inductive_package.ML"
 
 
 end
diff -r 520127b708e6 -r 07be4fccd329 progtutorial.pdf