COPYRIGHT
author dixon
Wed, 02 Mar 2005 10:33:10 +0100
changeset 15560 c862d556fb18
parent 14981 e73f8140af78
child 17547 b0d70cf4ed18
permissions -rw-r--r--
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
14981
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     3
Copyright (c) 2004,
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     4
  University of Cambridge and
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     5
  Technische Universitaet Muenchen.
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     6
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     7
  All rights reserved.
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     8
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
     9
Redistribution and use in source and binary forms, with or without 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    10
modification, are permitted provided that the following conditions are 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    11
met:
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    12
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    13
* Redistributions of source code must retain the above copyright 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    14
notice, this list of conditions and the following disclaimer.
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    15
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    16
* Redistributions in binary form must reproduce the above copyright 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    17
notice, this list of conditions and the following disclaimer in the 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    18
documentation and/or other materials provided with the distribution.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
14981
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    20
* Neither the name of the University of Cambridge or the Technical 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    21
University of Munich nor the names of their contributors may be used to 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    22
endorse or promote products derived from this software without specific 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    23
prior written permission.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
14981
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    25
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    26
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    27
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    28
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    29
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    30
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    31
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    32
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    33
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    34
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 14059
diff changeset
    35
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.