id	summary	status	owner	type	priority	milestone
38	integrate CASL consistency checker with Hets	assigned	mgross	task	critical	0.95
45	translate sort generation constraints to OMDoc	new	ewaryst	task	critical	1.0
50	make OMDoc interface logic independent	new	elena	task	critical	1.0
62	improve Isabelle default simplifier	new	till	task	critical	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
67	implement proof system for refinements	new	mcodescu	task	critical	0.95
72	Check correctness of referenced nodes in SimpleDatatypes.casl	new	till	bug	critical	0.95
114	merge or rename consCheck and cons_checkers	new	till	task	critical	0.95
131	Translation to Isabelle: let cases and classes	new	maeder	task	critical	0.95
171	sublogics based on theories?	new	mcodescu	feature	critical	0.95
172	signatures versus theories	new	mcodescu	feature	critical	0.95
225	check architectural parser	new	till	bug	critical	0.95
243	Improve Selection Possibilities of Sentences for Proofs	new	dodi	feature	critical	1.0
258	Clean up Mapping of G_theory	new	till	task	critical	0.95
301	adapt GPL warranty to German law	new	till	task	critical	0.95
311	keep structure when calling provers	new	maeder	task	critical	0.95
319	Create HTML info for Hets LiveCD	new	till	task	critical	0.95
345	restrict sublogic in comorphism from HasCASL to Isabelle	new	maeder	task	critical	0.95
357	Use existing Isabelle theories	new	luecke	task	critical	0.95
380	add descriptions to Modal, Taxonomy, CASL_DL, OWL_DL, ConstraintCASL, Comorphism modules	new	till	task	critical	0.95
383	type information ignored	new	maeder	bug	critical	0.95
417	develop heuristics for comorphism and prover selection	new	dodi	task	critical	0.95
427	recognize some generated types as conservative	assigned	mgross	task	critical	1.0
437	HasCASL subsort coding: make subsort graph explicit	reopened	maeder	task	critical	0.95
452	CoCasl - Isabelle tactics	new	hausmann	bug	critical	0.95
487	integrate Isabelle as a full logic node (also read in theories)	new	maeder	feature	critical	0.95
518	Connect Hets to SMV model checker (standalone version)	new	hartke	task	critical	0.95
519	Connect Hets to SMV model checker (full integration)	new	hartke	task	critical	0.95
528	update to OMDoc 1.6	new	ewaryst	bug	critical	0.95
549	mapping a partial op to a total one does not work for HasCASL	new	maeder	bug	critical	0.95
556	split module OMDoc/OMDocOutput.hs	new	elena	task	critical	0.95
558	Translating some HOFs from HasCASL to Isabelle fails	new	maeder	bug	critical	0.95
581	Keep structure when flattening out heterogeneity and renaming	new	stassiy	task	critical	0.95
589	optimize normal form computation	new	mcodescu	bug	critical	0.95
599	Shift proof goals against conservative extensions	new	dodi	task	critical	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
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
650	Obtain weakly amalgamable cocones via logic translations	new	mcodescu	feature	critical	0.95
652	Consistency check for architectural specifications	new	mcodescu	feature	critical	0.95
686	Look at THF and integrate Leo-II	new	luecke	task	critical	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
701	Allow the import of files with separate DG interface (OWL, Haskell, ...)	new	till	task	critical	0.95
721	Warn in case of unsoundness and/or incompleteness	new	luecke	feature	critical	0.95
725	Incremental static analysis and dg proof reconstruction	assigned	maeder	task	critical	0.95
727	provide additional commands for hets -I -x	new	maeder	task	critical	0.95
728	Annotate DGOrigin datatype with proof script information	new	maeder	task	critical	0.95
9	SPASS problem with reverse of lists	new	till	bug	major	0.95
16	improve dependency tracking for development graph proofs	new	maeder	feature	major	0.95
17	Implement weakly amalgamable cocones	new	mcodescu	task	major	0.95
26	Enforce sublanguage syntax	new	maeder	feature	major	1.0
28	search function for theories / dg nodes	assigned	normann	task	major	1.0
29	check proof datastructures for use with informal proofs	new	normann	task	major	1.0
31	translation Modal-CASL <-> CASL-DL	new	codruta	task	major	1.0
32	improve ModalCASL	new	codruta	task	major	1.0
33	proofs with CASL basic datatypes	new	luecke	task	major	0.95
41	unify URLs in OMDoc and Hets	new	ewaryst	task	major	1.0
47	introduce an OMDoc symbol for sort definitions	new	ewaryst	task	major	1.0
48	check origin of OMDoc symbols	new	ewaryst	task	major	1.0
49	correct translation of hiding when translating Hets <-> OMDoc	new	ewaryst	bug	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
55	generate (x)html code from Doc	new	maeder	task	major	1.0
59	change management	new	maeder	feature	major	0.95
64	improve efficiency of static analysis of architectural specifications	new	till	task	major	1.0
68	implement institution morphisms	new	mcodescu	task	major	1.0
69	Maude as logic in Hets	new	mkhl	task	major	0.95
70	Integrate model checkers	new	till	task	major	1.0
73	enhance web interface	new	till	feature	major	1.0
74	translation of proofs along comorphisms	new	mcodescu	task	major	0.95
80	Display umlauts in uDrawGraph	new	maeder	bug	major	1.0
82	Check OMDoc coding of subsorts	new	normann	task	major	0.95
83	Complete coding of Haskell in Isabelle	new	paolot	task	major	0.95
86	weakly amalgamable cocones for heterogeneous diagrams	new	mcodescu	task	major	0.95
87	Implement institution comorphism modifications	new	mcodescu	task	major	0.95
89	HideTheoremShift: automatically generate conservative extensions	new	mcodescu	task	major	1.0
91	.dg files: store only current library; import .dg files for other libraries	new	maeder	task	major	1.0
99	send XML queries with DCC expressions to SparQ	new	luecke	bug	major	0.95
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
103	test reading and writing ConstraintCASL composition tables in QGR/XML and SparQ formats	new	till	task	major	0.95
104	qualitative algebra toolset	new	till	task	major	0.95
107	Write institution for ConstraintCASL	new	till	task	major	0.95
115	improve handling of compositions of comorphisms	new	mcodescu	task	major	0.95
116	check potential use of metavariables	new	till	task	major	1.0
117	adapt terminology for symbols	new	mcodescu	task	major	2.0
130	allow naming of subgraphs of dg	new	raider	task	major	1.0
133	Pattern analysis for program equations	new	maeder	task	major	0.95
136	Create Isabelle theory morphisms from hets theorem links	new	maeder	task	major	1.0
137	Improve Isabelle interface	new	maeder	task	major	0.95
139	proof rules for free theorem links	new	till	task	major	1.0