COPYRIGHT
author wenzelm
Wed, 02 Aug 2006 22:27:04 +0200
changeset 20310 6cb47e95a74b
parent 17547 b0d70cf4ed18
child 24798 d04aaadfd7ae
permissions -rw-r--r--
normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; prems_limit: < 0 means no output; added debug option (back from proof_display.ML);
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
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 14981
diff changeset
     3
Copyright (c) 2005,
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
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.