# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1300306483 -3600
# Node ID a5da7b6aff8fe3cd0ed0fb06e202d166576da100
# Parent  6aa98a113e6c8558a5dcec26986f5c0dbb2cfd27
precise path to LaTeXsugar

diff -r 6aa98a113e6c -r a5da7b6aff8f Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 16 21:07:50 2011 +0100
+++ b/Paper/Paper.thy	Wed Mar 16 21:14:43 2011 +0100
@@ -1,6 +1,7 @@
 (*<*)
 theory Paper
-imports "../Nominal/Nominal2" "LaTeXsugar"
+imports "../Nominal/Nominal2" 
+        "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 consts
diff -r 6aa98a113e6c -r a5da7b6aff8f Paper/ROOT.ML
--- a/Paper/ROOT.ML	Wed Mar 16 21:07:50 2011 +0100
+++ b/Paper/ROOT.ML	Wed Mar 16 21:14:43 2011 +0100
@@ -1,3 +1,4 @@
 quick_and_dirty := true;
-no_document use_thys ["LaTeXsugar", "../Nominal/Nominal2"];
+no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", 
+                      "../Nominal/Nominal2"];
 use_thys ["Paper"];
\ No newline at end of file
diff -r 6aa98a113e6c -r a5da7b6aff8f Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Wed Mar 16 21:07:50 2011 +0100
+++ b/Pearl-jv/Paper.thy	Wed Mar 16 21:14:43 2011 +0100
@@ -3,7 +3,7 @@
 imports "../Nominal/Nominal2_Base" 
         "../Nominal/Atoms" 
         "../Nominal/Nominal2_Abs"
-        "LaTeXsugar"
+        "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 abbreviation
diff -r 6aa98a113e6c -r a5da7b6aff8f Pearl-jv/ROOT.ML
--- a/Pearl-jv/ROOT.ML	Wed Mar 16 21:07:50 2011 +0100
+++ b/Pearl-jv/ROOT.ML	Wed Mar 16 21:14:43 2011 +0100
@@ -2,4 +2,4 @@
 use_thys ["../Nominal/Nominal2_Base", 
           "../Nominal/Atoms", 
           "../Nominal/Nominal2_Abs",
-          "LaTeXsugar"];
+          "~~/src/HOL/Library/LaTeXsugar"];
diff -r 6aa98a113e6c -r a5da7b6aff8f Pearl/Paper.thy
--- a/Pearl/Paper.thy	Wed Mar 16 21:07:50 2011 +0100
+++ b/Pearl/Paper.thy	Wed Mar 16 21:14:43 2011 +0100
@@ -2,7 +2,7 @@
 theory Paper
 imports "../Nominal/Nominal2_Base" 
         "../Nominal/Atoms" 
-        "LaTeXsugar"
+        "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 notation (latex output)
diff -r 6aa98a113e6c -r a5da7b6aff8f Pearl/ROOT.ML
--- a/Pearl/ROOT.ML	Wed Mar 16 21:07:50 2011 +0100
+++ b/Pearl/ROOT.ML	Wed Mar 16 21:14:43 2011 +0100
@@ -1,5 +1,5 @@
 no_document use_thys ["../Nominal/Nominal2_Base", 
                       "../Nominal/Atoms", 
-                      "LaTeXsugar"];
+                      "~~/src/HOL/Library/LaTeXsugar"];
 
 use_thys ["Paper"];
\ No newline at end of file
diff -r 6aa98a113e6c -r a5da7b6aff8f Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Mar 16 21:07:50 2011 +0100
+++ b/Quotient-Paper/Paper.thy	Wed Mar 16 21:14:43 2011 +0100
@@ -1,8 +1,8 @@
 (*<*)
 theory Paper
 imports "Quotient" "Quotient_Syntax"
-        "LaTeXsugar"
-        "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet"
+        "~~/src/HOL/Library/LaTeXsugar"
+        "~~/src/HOL/Quotient_Examples/FSet"
 begin
 
 (****
diff -r 6aa98a113e6c -r a5da7b6aff8f Quotient-Paper/ROOT.ML
--- a/Quotient-Paper/ROOT.ML	Wed Mar 16 21:07:50 2011 +0100
+++ b/Quotient-Paper/ROOT.ML	Wed Mar 16 21:14:43 2011 +0100
@@ -1,5 +1,5 @@
 quick_and_dirty := true;
 no_document use_thys ["Quotient", 
-                      "LaTeXsugar",
-                      "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" ];
+                      "~~/src/HOL/Library/LaTeXsugar",
+                      "~~/src/HOL/Quotient_Examples/FSet" ];
 use_thys ["Paper"];