Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
precise path to LaTeXsugar
authorChristian Urban <urbanc@in.tum.de>
Wed, 16 Mar 2011 21:14:43 +0100
changeset 2747 a5da7b6aff8f
parent 2746 6aa98a113e6c
child 2748 6f38e357b337
precise path to LaTeXsugar
Paper/Paper.thy file | annotate | diff | comparison | revisions
Paper/ROOT.ML file | annotate | diff | comparison | revisions
Pearl-jv/Paper.thy file | annotate | diff | comparison | revisions
Pearl-jv/ROOT.ML file | annotate | diff | comparison | revisions
Pearl/Paper.thy file | annotate | diff | comparison | revisions
Pearl/ROOT.ML file | annotate | diff | comparison | revisions
Quotient-Paper/Paper.thy file | annotate | diff | comparison | revisions
Quotient-Paper/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
--- 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
--- 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"];
--- 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)
--- 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
--- 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
 
 (****
--- 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"];
nominal2