equal
deleted
inserted
replaced
1 (* Title: ZF/UNITY/Monotonicity.thy |
1 (* Title: ZF/UNITY/Monotonicity.thy |
2 ID: $Id \<in> Monotonicity.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4 Copyright 2002 University of Cambridge |
3 Copyright 2002 University of Cambridge |
5 |
4 |
6 Monotonicity of an operator (meta-function) with respect to arbitrary set relations. |
5 Monotonicity of an operator (meta-function) with respect to arbitrary |
|
6 set relations. |
7 *) |
7 *) |
8 |
8 |
9 header{*Monotonicity of an Operator WRT a Relation*} |
9 header{*Monotonicity of an Operator WRT a Relation*} |
10 |
10 |
11 theory Monotonicity imports GenPrefix MultisetSum |
11 theory Monotonicity imports GenPrefix MultisetSum |