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.
Notation available locally
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 11 Feb 2010 14:00:00 +0100
changeset 1129 9a86f0ef6503
parent 1128 17ca92ab4660
child 1130 fb5f5735a426
Notation available locally
Quot/Examples/LarryDatatype.thy file | annotate | diff | comparison | revisions
Quot/Nominal/LFex.thy file | annotate | diff | comparison | revisions
Quot/Nominal/LamEx.thy file | annotate | diff | comparison | revisions
Quot/Nominal/LamEx2.thy file | annotate | diff | comparison | revisions
Quot/Nominal/Terms.thy file | annotate | diff | comparison | revisions
Quot/Quotient.thy file | annotate | diff | comparison | revisions
Quot/Quotient_List.thy file | annotate | diff | comparison | revisions
Quot/Quotient_Option.thy file | annotate | diff | comparison | revisions
Quot/Quotient_Product.thy file | annotate | diff | comparison | revisions
Quot/Quotient_Sum.thy file | annotate | diff | comparison | revisions 
--- 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*}
--- 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
--- 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
--- 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
--- 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
--- 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
 
--- 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. *}
--- 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. *}
--- 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. *}
--- 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. *}
nominal2