COPYRIGHT
author blanchet
Tue, 27 Apr 2010 11:24:47 +0200
changeset 36473 8a5c99a1c965
parent 30895 bad26d8f0adf
child 37159 07f3f5a03e98
permissions -rw-r--r--
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
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
30895
bad26d8f0adf updated for Isabelle2009;
wenzelm
parents: 27306
diff changeset
     3
Copyright (c) 2009,
14981
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
27306
0609faccb903 updated for 2008;
wenzelm
parents: 24798
diff changeset
    20
* Neither the name of the University of Cambridge or the Technische
0609faccb903 updated for 2008;
wenzelm
parents: 24798
diff changeset
    21
Universitaet Muenchen nor the names of their contributors may be used
0609faccb903 updated for 2008;
wenzelm
parents: 24798
diff changeset
    22
to endorse or promote products derived from this software without
0609faccb903 updated for 2008;
wenzelm
parents: 24798
diff changeset
    23
specific 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.