Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 298315 Details for
Bug 397995
isabelle proof assistant
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
metadata with package and use flag descriptions
metadata.xml (text/plain), 1.82 KB, created by
Mark Wright
on 2012-01-08 12:33:40 UTC
(
hide
)
Description:
metadata with package and use flag descriptions
Filename:
MIME Type:
Creator:
Mark Wright
Created:
2012-01-08 12:33:40 UTC
Size:
1.82 KB
patch
obsolete
><?xml version="1.0" encoding="UTF-8"?> ><!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> ><pkgmetadata> ><herd>sci-mathematics</herd> ><longdescription lang='en'> >Isabelle is a generic proof assistant. It allows mathematical >formulas to be expressed in a formal language and provides tools >for proving those formulas in a logical calculus. The main >application is the formalization of mathematical proofs and in >particular formal verification, which includes proving the >correctness of computer hardware or software and proving >properties of computer languages and protocols. ></longdescription> ><use> > <flag name='Pure'>Pure is the basis for all object-logics.</flag> > <flag name='FOL'>FOL (Many-sorted First-Order Logic) provides basic > classical and intuitionistic first-order logic. It is polymorphic.</flag> > <flag name='HOL'>(Higher-Order Logic) is a version of classical higher-order > logic resembling that of the HOL System.</flag> > <flag name='ZF'>ZF (Set Theory) offers a formulation of Zermelo-Fraenkel > set theory on top of FOL.</flag> > <flag name='CCL'>CCL (Classical Computational Logic)</flag> > <flag name='CTT'>CTT (Constructive Type Theory) is an extensional version > of Martin-Löf's Type Theory.</flag> > <flag name='Cube'>Cube (The Lambda Cube)</flag> > <flag name='FOLP'>FOLP (FOL with Proof Terms)</flag> > <flag name='LCF'>LCF (Logic of Computable Functions)</flag> > <flag name='Sequents'>Sequents (first-order, modal and linear logics)</flag> > <flag name='graphbrowsing'>Generate theory browsing information, > including HTML documents that show a theory's definition, the > theorems proved in its ML file and the relationship with its > ancestors and descendants.</flag> > <flag name='proofgeneral'>Add support for the > <pkg>app-emacs/proofgeneral</pkg> proof assistant front end.</flag> ></use> ></pkgmetadata>
You cannot view the attachment while viewing its details because your browser does not support IFRAMEs.
View the attachment on a separate page
.
View Attachment As Raw
Actions:
View
Attachments on
bug 397995
:
298313
| 298315 |
298317
|
298319