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.
FSet changes for Qpaper
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 28 Oct 2010 14:12:30 +0900
changeset 2551 26d594a9b89f
parent 2550 551c5a8b6b2c
child 2552 bf4b28ebb412
FSet changes for Qpaper
Quotient-Paper/Paper.thy file | annotate | diff | comparison | revisions
Quotient-Paper/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/Quotient-Paper/Paper.thy	Thu Oct 28 14:03:46 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Thu Oct 28 14:12:30 2010 +0900
@@ -2,7 +2,7 @@
 theory Paper
 imports "Quotient" "Quotient_Syntax"
         "LaTeXsugar"
-        "../Nominal/FSet"
+        "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet"
 begin
 
 (****
--- a/Quotient-Paper/ROOT.ML	Thu Oct 28 14:03:46 2010 +0900
+++ b/Quotient-Paper/ROOT.ML	Thu Oct 28 14:12:30 2010 +0900
@@ -1,6 +1,5 @@
 quick_and_dirty := true;
 no_document use_thys ["Quotient", 
                       "LaTeXsugar",
-                      "../Nominal/FSet" ];
-
-use_thys ["Paper"];
\ No newline at end of file
+                      "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" ];
+use_thys ["Paper"];
nominal2