# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1300413194 -3600
# Node ID 4532577b61e014593460258f43ed952b12778529
# Parent  242e81f4d461c8685b2e1a8a922ea98b26f0acae
updated to new Isabelle

diff -r 242e81f4d461 -r 4532577b61e0 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Wed Feb 23 23:55:37 2011 +0000
+++ b/ProgTutorial/Base.thy	Fri Mar 18 02:53:14 2011 +0100
@@ -1,5 +1,6 @@
 theory Base
-imports Main LaTeXsugar
+imports Main 
+        "~~/src/HOL/Library/LaTeXsugar"
 uses
   ("output_tutorial.ML")
   ("antiquote_setup.ML")
diff -r 242e81f4d461 -r 4532577b61e0 ProgTutorial/ROOT.ML
--- a/ProgTutorial/ROOT.ML	Wed Feb 23 23:55:37 2011 +0000
+++ b/ProgTutorial/ROOT.ML	Fri Mar 18 02:53:14 2011 +0100
@@ -3,7 +3,7 @@
 no_document use_thy "Base";
 no_document use_thy "Package/Simple_Inductive_Package";
 no_document use_thy "~~/src/HOL/Number_Theory/Primes"; 
-no_document use_thy "Efficient_Nat";
+no_document use_thy "~~/src/HOL/Library/Efficient_Nat";
 
 use_thy "Intro";
 use_thy "First_Steps";
diff -r 242e81f4d461 -r 4532577b61e0 ProgTutorial/Recipes/CallML.thy
--- a/ProgTutorial/Recipes/CallML.thy	Wed Feb 23 23:55:37 2011 +0000
+++ b/ProgTutorial/Recipes/CallML.thy	Fri Mar 18 02:53:14 2011 +0100
@@ -1,6 +1,7 @@
 (*<*)
 theory CallML
-imports "~~/src/HOL/Number_Theory/Primes" Efficient_Nat
+imports "~~/src/HOL/Number_Theory/Primes" 
+        "~~/src/HOL/Library/Efficient_Nat"
 begin
 (*>*)
 
diff -r 242e81f4d461 -r 4532577b61e0 progtutorial.pdf
Binary file progtutorial.pdf has changed