# HG changeset patch
# User webertj
# Date 1364312491 -3600
# Node ID a8724924a62ecfa08eb22208dcf5d63eaae33f43
# Parent  0f76f481dbb5b9fa2773a7428be23bfe216fa226
Manual merge of d121bd2a5a47 from Isabelle/AFP.

diff -r 0f76f481dbb5 -r a8724924a62e Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Mar 11 16:37:54 2013 +0000
+++ b/Nominal/Nominal2_Base.thy	Tue Mar 26 16:41:31 2013 +0100
@@ -1056,11 +1056,11 @@
   given.
 *}
 
-class le_eqvt =  order + 
-  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))"
-
-class inf_eqvt = complete_lattice +
-  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, Inf}) set))"
+class le_eqvt = ord +
+  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{order, pt}))))"
+
+class inf_eqvt = Inf +
+  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::'a::{complete_lattice, pt} set))"
 
 instantiation bool :: le_eqvt
 begin