# HG changeset patch # User Christian Urban # Date 1274880934 -7200 # Node ID 762a739c9eb477980a079c6d86cc05f7ad517f7e # Parent 1cf20169660c6989bd4076d1e27fbd618f10834f added FSet to the correct paper diff -r 1cf20169660c -r 762a739c9eb4 Paper/Paper.thy --- a/Paper/Paper.thy Wed May 26 15:26:22 2010 +0200 +++ b/Paper/Paper.thy Wed May 26 15:35:34 2010 +0200 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports "../Nominal/Test" "../Nominal/FSet" "LaTeXsugar" +imports "../Nominal/Test" "LaTeXsugar" begin consts diff -r 1cf20169660c -r 762a739c9eb4 Paper/ROOT.ML --- a/Paper/ROOT.ML Wed May 26 15:26:22 2010 +0200 +++ b/Paper/ROOT.ML Wed May 26 15:35:34 2010 +0200 @@ -1,3 +1,3 @@ quick_and_dirty := true; -no_document use_thys ["LaTeXsugar", "../Nominal/FSet"]; +no_document use_thys ["LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file diff -r 1cf20169660c -r 762a739c9eb4 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Wed May 26 15:26:22 2010 +0200 +++ b/Quotient-Paper/Paper.thy Wed May 26 15:35:34 2010 +0200 @@ -2,6 +2,7 @@ theory Paper imports "Quotient" "LaTeXsugar" + "../Nominal/FSet" begin notation (latex output) diff -r 1cf20169660c -r 762a739c9eb4 Quotient-Paper/ROOT.ML --- a/Quotient-Paper/ROOT.ML Wed May 26 15:26:22 2010 +0200 +++ b/Quotient-Paper/ROOT.ML Wed May 26 15:35:34 2010 +0200 @@ -1,4 +1,5 @@ no_document use_thys ["Quotient", - "LaTeXsugar"]; + "LaTeXsugar", + "../Nominal/FSet" ]; use_thys ["Paper"]; \ No newline at end of file