| #9 |
SPASS problem with reverse of lists
|
new
|
till
|
bug
|
major
|
0.95
|
| #49 |
correct translation of hiding when translating Hets <-> OMDoc
|
new
|
ewaryst
|
bug
|
major
|
1.0
|
| #72 |
Check correctness of referenced nodes in SimpleDatatypes.casl
|
new
|
till
|
bug
|
critical
|
0.95
|
| #80 |
Display umlauts in uDrawGraph
|
new
|
maeder
|
bug
|
major
|
1.0
|
| #99 |
send XML queries with DCC expressions to SparQ
|
new
|
luecke
|
bug
|
major
|
0.95
|
| #179 |
Strategies for development graph rules
|
new
|
dodi
|
bug
|
major
|
0.95
|
| #191 |
(sort of) second order type unification
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #225 |
check architectural parser
|
new
|
till
|
bug
|
critical
|
0.95
|
| #226 |
fix error handling in Static.AnalysisArchitecture
|
new
|
mcodescu
|
bug
|
major
|
0.95
|
| #234 |
improve Static.LogicStructured
|
new
|
till
|
bug
|
major
|
1.0
|
| #256 |
Modal2CASL defects
|
new
|
codruta
|
bug
|
major
|
0.95
|
| #324 |
LCF-like abstraction barrier for development graph calculus
|
new
|
till
|
bug
|
major
|
1.0
|
| #383 |
type information ignored
|
new
|
maeder
|
bug
|
critical
|
0.95
|
| #390 |
Pretty printing CspCASL processes lacks parentheses
|
assigned
|
gimblett
|
bug
|
minor
|
1.0
|
| #403 |
sentence names also need to be renamed by comorphisms
|
new
|
maeder
|
bug
|
minor
|
0.95
|
| #419 |
Haskell2Isabelle: treatment of (non-)strict datatypes and newtypes
|
new
|
paolot
|
bug
|
major
|
0.95
|
| #433 |
reparsing theory files does not work
|
new
|
maeder
|
bug
|
minor
|
0.95
|
| #452 |
CoCasl - Isabelle tactics
|
new
|
hausmann
|
bug
|
critical
|
0.95
|
| #456 |
extendMorphism goes wrong for Categories.het
|
new
|
maeder
|
bug
|
minor
|
0.95
|
| #462 |
Development graph calculus takes too long
|
new
|
mcodescu
|
bug
|
major
|
0.95
|
| #527 |
CDs for logics
|
new
|
elena
|
bug
|
major
|
0.95
|
| #528 |
update to OMDoc 1.6
|
new
|
ewaryst
|
bug
|
critical
|
0.95
|
| #531 |
refactor casl.omdoc with other logics
|
new
|
ewaryst
|
bug
|
major
|
0.95
|
| #549 |
mapping a partial op to a total one does not work for HasCASL
|
new
|
maeder
|
bug
|
critical
|
0.95
|
| #550 |
Haskell to Isabelle HOLCF failure
|
new
|
paolot
|
bug
|
major
|
0.95
|
| #551 |
Proofs -> Automatic on Basic/LinearAlgebra_I.casl freezes GUI
|
new
|
till
|
bug
|
minor
|
0.95
|
| #558 |
Translating some HOFs from HasCASL to Isabelle fails
|
new
|
maeder
|
bug
|
critical
|
0.95
|
| #562 |
reading omdoc files takes too much memory
|
new
|
elena
|
bug
|
major
|
0.95
|
| #569 |
adjust HasCASL to overview
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #570 |
better support domains and program blocks
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #583 |
different logics in imports, formal and actual specs still cause problems
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #584 |
extension removes alias created for (non-atomic) subtype
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #585 |
SoftFOL and SuleCFOL2SoftFOL problems
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #586 |
finality test fails
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #589 |
optimize normal form computation
|
new
|
mcodescu
|
bug
|
critical
|
0.95
|
| #595 |
Integrate OnePoint
|
new
|
till
|
bug
|
major
|
0.95
|
| #600 |
casl-mode goes wrong after '\"'
|
new
|
luecke
|
bug
|
major
|
0.95
|
| #610 |
Make dg menus more robust
|
new
|
till
|
bug
|
critical
|
0.95
|
| #611 |
Modal systems cannot be translated to CASL
|
new
|
codruta
|
bug
|
critical
|
0.95
|
| #612 |
warn when theory has been reduced
|
new
|
luecke
|
bug
|
critical
|
0.95
|
| #616 |
Filename extension is ignored
|
new
|
till
|
bug
|
critical
|
0.95
|
| #618 |
Proving with (co)free links does not work correctly
|
new
|
luecke
|
bug
|
critical
|
0.95
|
| #624 |
QuickCheck erroneously disproves contradiction
|
new
|
till
|
bug
|
critical
|
0.95
|
| #627 |
Proofs->Automatic fails for RelationAlgebraModel
|
new
|
till
|
bug
|
major
|
0.95
|
| #628 |
Termination proof produces error
|
new
|
luecke
|
bug
|
major
|
0.95
|
| #630 |
improve HasCASL typechecking speed
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #636 |
HasCASL theory computation problem
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #640 |
Encoding of Sort Generation Constraints in Isabelle
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #645 |
Make injections be identities in SuleCFOL2SoftFOL
|
new
|
till
|
bug
|
critical
|
0.95
|
| #648 |
Improve interaction of hiding and normal forms
|
new
|
mcodescu
|
bug
|
critical
|
0.95
|
| #649 |
Colimiting cocone includes a non-signature morphism
|
new
|
mcodescu
|
bug
|
critical
|
0.95
|
| #664 |
HasCASL subtype relation and membership problem
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #676 |
Integrate Fact++ as consistency checker into Hets
|
assigned
|
shabani
|
bug
|
major
|
0.95
|
| #681 |
"Prove" on a node enlarges local theory
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #683 |
flattening disjoint union is incomplete
|
new
|
stassiy
|
bug
|
major
|
0.95
|
| #684 |
hets crashes when trying to prove PropTrue with zchaff or minisat
|
new
|
luecke
|
bug
|
major
|
0.95
|
| #692 |
Axioms from unit, assoc, comm annotations are not exported from HasCASL specs to Isabelle
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #694 |
Add headlines to different parts of truth tables for truth table prover
|
new
|
till
|
bug
|
critical
|
0.95
|
| #695 |
Partiality translations
|
new
|
maeder
|
bug
|
critical
|
0.95
|
| #707 |
Have a look at model finder Nitpick
|
new
|
luecke
|
bug
|
major
|
0.95
|
| #714 |
Compositional reasoning in Coloss
|
new
|
hausmann
|
bug
|
major
|
0.95
|
| #720 |
Vampire does not return used axioms
|
new
|
luecke
|
bug
|
major
|
0.95
|
| #736 |
Prover Isabelle is not supported in CMDL mode
|
new
|
till
|
bug
|
major
|
0.95
|
| #737 |
XML parsing creates wrong CMDL commands as text
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #739 |
proofs run by the CMDL are not recorded in the development graph
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #742 |
for concurrent proofs the output is intermangled
|
new
|
luecke
|
bug
|
minor
|
1.0
|
| #746 |
parsing Maude modules
|
new
|
adrian
|
bug
|
major
|
0.95
|
| #760 |
Wrong proof created by extra options passed to darwin
|
new
|
maeder
|
bug
|
major
|
0.95
|
| #16 |
improve dependency tracking for development graph proofs
|
new
|
maeder
|
feature
|
major
|
0.95
|
| #26 |
Enforce sublanguage syntax
|
new
|
maeder
|
feature
|
major
|
1.0
|
| #52 |
highlight instantiation diagrams
|
new
|
raider
|
feature
|
major
|
1.0
|
| #53 |
hide nodes that are far away
|
new
|
raider
|
feature
|
major
|
1.0
|
| #59 |
change management
|
new
|
maeder
|
feature
|
major
|
0.95
|
| #65 |
proof system for architectural specifications
|
new
|
mcodescu
|
feature
|
critical
|
0.95
|
| #66 |
implement static analysis of refinements
|
new
|
mcodescu
|
feature
|
critical
|
0.95
|
| #73 |
enhance web interface
|
new
|
till
|
feature
|
major
|
1.0
|
| #100 |
write ConstraintCASL composition tables to SparQ format
|
new
|
till
|
feature
|
major
|
0.95
|
| #101 |
write ConstraintCASL composition tables to Freiburg GQR XML format
|
new
|
till
|
feature
|
major
|
0.95
|
| #102 |
read ConstraintCASL composition tables from Freiburg GQR XML format
|
new
|
till
|
feature
|
major
|
0.95
|
| #148 |
ontology mediation via pushouts/pullbacks/pulations
|
new
|
luecke
|
feature
|
major
|
1.0
|
| #150 |
lift theorem links between same instances of different parameterized specs
|
new
|
till
|
feature
|
major
|
1.0
|
| #151 |
node and link menu for conservativity status
|
new
|
till
|
feature
|
major
|
1.0
|
| #152 |
show subgraphs of the development graph
|
new
|
till
|
feature
|
major
|
1.0
|
| #153 |
globally display nodes containing symbols mapped twice
|
new
|
till
|
feature
|
major
|
1.0
|
| #158 |
Automatic GUI and CMDL interface for Isabelle
|
new
|
maeder
|
feature
|
minor
|
1.0
|
| #169 |
sublogic translation table
|
new
|
dodi
|
feature
|
major
|
0.95
|
| #171 |
sublogics based on theories?
|
new
|
mcodescu
|
feature
|
critical
|
0.95
|
| #172 |
signatures versus theories
|
new
|
mcodescu
|
feature
|
critical
|
0.95
|
| #180 |
Add provers for modal logic
|
new
|
codruta
|
feature
|
major
|
0.95
|
| #187 |
interactive typing of expressions
|
new
|
rpascanu
|
feature
|
major
|
0.95
|
| #210 |
display minimal types of an operation symbol in CASL
|
new
|
maeder
|
feature
|
major
|
1.0
|
| #243 |
Improve Selection Possibilities of Sentences for Proofs
|
new
|
dodi
|
feature
|
critical
|
1.0
|
| #245 |
Improve Taxonomy Display for CASL
|
new
|
raider
|
feature
|
minor
|
1.0
|
| #254 |
Provide Goals for Sort Generation Axioms
|
new
|
maeder
|
feature
|
minor
|
0.95
|
| #255 |
Add Default Comorphism from Modal Logic to SoftFOL
|
new
|
codruta
|
feature
|
minor
|
0.95
|
| #295 |
Integrate IsaPlanner into Hets
|
new
|
dodi
|
feature
|
major
|
0.95
|
| #296 |
Integrate Hets with PGIP-Plugin for Eclipse
|
new
|
rpascanu
|
feature
|
minor
|
1.0
|
| #298 |
add a logic OMDoc-PUN
|
new
|
ewaryst
|
feature
|
major
|
0.95
|
| #300 |
process algebras
|
new
|
maeder
|
feature
|
major
|
1.0
|
| #323 |
Add sorting to Prover Windows
|
new
|
raider
|
feature
|
minor
|
0.95
|