# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265893200 -3600
# Node ID 9a86f0ef65034ff418b51a297fe7c215ce8c03bd
# Parent  17ca92ab4660e4ba1e5191ae890b7cbe11c94c40
Notation available locally

diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -1,5 +1,5 @@
 theory LarryDatatype
-imports Main "../Quotient"
+imports Main "../Quotient" "../Quotient_Syntax"
 begin
 
 subsection{*Defining the Free Algebra*}
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -1,5 +1,5 @@
 theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient"  "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
 begin
 
 atom_decl name
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -1,5 +1,5 @@
 theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
 begin
 
 atom_decl name
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -1,5 +1,5 @@
 theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs" "../Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
 begin
 
 atom_decl name
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
 begin
 
 atom_decl name
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Quotient.thy
--- a/Quot/Quotient.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Quotient.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -798,5 +798,10 @@
   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   {* lifts theorems to quotient types *}
 
+no_notation
+  rel_conj (infixr "OOO" 75) and
+  fun_map (infixr "--->" 55) and
+  fun_rel (infixr "===>" 55)
+
 end
 
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Quotient_List.thy
--- a/Quot/Quotient_List.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Quotient_List.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 theory Quotient_List
-imports Quotient List
+imports Quotient Quotient_Syntax List
 begin
 
 section {* Quotient infrastructure for the list type. *}
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Quotient_Option.thy
--- a/Quot/Quotient_Option.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Quotient_Option.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 theory Quotient_Option
-imports Quotient
+imports Quotient Quotient_Syntax
 begin
 
 section {* Quotient infrastructure for the option type. *}
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Quotient_Product.thy
--- a/Quot/Quotient_Product.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Quotient_Product.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 theory Quotient_Product
-imports Quotient
+imports Quotient Quotient_Syntax
 begin
 
 section {* Quotient infrastructure for the product type. *}
diff -r 17ca92ab4660 -r 9a86f0ef6503 Quot/Quotient_Sum.thy
--- a/Quot/Quotient_Sum.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Quotient_Sum.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 theory Quotient_Sum
-imports Quotient
+imports Quotient Quotient_Syntax
 begin
 
 section {* Quotient infrastructure for the sum type. *}