todo revision d4f60a7dc41e0430d16c79f0d156e556d6d1ba37
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHaskell parser f�r XHaskell erweitern
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDimplom: Encoding for HasCASL in Isabelle/HOL(CF)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskidevelopment graph calculus
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- Stack overflow for "show just subtree"
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitype check for CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski*** Error encode.casl:8.30, No correct typing for
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiTest auf Einpunkt-Modell
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski (ein Datenelement, wahre Pr�dikate, totale Funktionen)
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski************************************************
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiZicheng (Till)
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski************************************************
ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiTranslation from CASL with subsorts to CASL without subsorts
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskisee CATS/basic_encode.sml, encode SubCFOL into CFOL
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiencode subsorting by injection functions
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski1. translation of signatures (see HetCATS/CASL/Sign.hs)
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski2. genertion of axioms (injectivity, overloading ...)
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskidetails: see paper in Theoretical Computer Science, p. 407
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski************************************************
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski************************************************
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiLaTeX pretty printer
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskivon Christian:
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskia) analysierte Formeln und Terme optimal/k�rzer ausgeben:
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskishorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskimit dem Ergebnistyp qualifiziert.
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski((a: Nat) + (b: Nat)): Nat
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskib) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskif�r die CASL Datentypen zu bekommen.
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski************************************************
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski************************************************
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiMissing points for heterogeneous WADT 04 example:
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski- improve display of HasCASL sigs + mors
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiStatic analysis for HasCASL
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski checking class constraints of terms
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski pattern analysis for program equations
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski - for simple types (currently type synonyms)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski symbol representation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski symbol map analysis (hiding sub/supertypes)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeak amalgamation analysis?
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiInstantiate Transformation Application system for HasCASL?
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiProofs in HasCASL
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski************************************************
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski************************************************
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskivisualization of "taxonomy" of CASL signatures
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiRecognize guarded fragment of CASL:
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski | exists x . At(x) /\ G
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBeweise in Isabelle
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Vorbild: Larch-Handbuch)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiParser and static analysis for CSP-CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederIsaWin: support CASL-libraries
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder************************************************
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis of architectural specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- correct display of CASL sublogis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- extended globDecomp rule: existing local Thm links
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (e.g. generated by %implied) should lead to fewer new local
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski links ("local composition" rule)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Improve adapation to Isabelle's lexis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski free datatypes
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski prove local thm link (=> green)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski better interaction between Isabelle instance (for one node)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + selection of single goals that are proved
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski => use PGIP interface (Christoph, David)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski correct show theory
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL-like syntax
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL annotation for lemmas that should be used in proof
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski inherit CASL's mixfix syntax
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicomp(id,x)=x for comorphism names
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGeneralie CASL2Modal
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMixfix analysis + typecheck for modality axiomatizations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski+ translations (e.g. modal to FOL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiComorphisms: also map of theories; with default definition
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL->Haskell with free DTs (mark sortgens) + recursion
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCoding of subsorts as unary predicates (for ontologies)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- List[Dec] wird List[Pos]
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- George wg. Schlie�en von Fenstern
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill Mossakowski- node numbers do not match
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill Mossakowski- thm links with external target should be provable as well
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill MossakowskiRemove warnings
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill MossakowskiDifferent types of logic translations
f1ba3c4b1394e88800bece2e9067e2866015cfebTill MossakowskiImprove Static analysis of structured specs
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiDevelopment graph calculus, Strategies for DG rules
f1ba3c4b1394e88800bece2e9067e2866015cfebTill MossakowskiManagement of change
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiIntegrate provers
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski Otter model checker
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski FOL-prover by Uli Furhbach
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski Isabelle codings: www.inf.ethz.ch/~vigano
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Renate Schmidt, Manchester: uses FOL prover for description logic
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski (as efficient as DL-specific tools!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Look at PROSPER toolkit
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski consistency: see IJCAR-workshop on non-provability in Cork
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski IJCAR workshop about logical frameworks and meta-languages
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus' wayfinding example
e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiUniForM workbench:
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowskivariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski Grothendieck logic)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski re-use ML signatures) (Einar)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDisplay Specs as daVinci subgraphs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInput text window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProver windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHets Web interface (cf. CATS/web_interface2.sml)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPackaging of installation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiintegrate QuickCheck
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGUI (vgl. VSE)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiincrease performance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemaining things
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Coq, PTT in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProof general interface (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTest Maya with basic datatypes
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVerbesserung der Fehlermeldungen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove encoding: CATS/basic_encode.sml (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExample of Agnes und Frank: proofs in HOL-CASL (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExamples for cond rewriting -> Christophe
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured free (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured cofree (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt Isabelle unions to CASL unions (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGenerate Proof obligations (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdd renaming to Isabelle kernel (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRepository mit korrekten und fehlerhaften Specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiComparsion of parsers (ML-yacc parser, SDF-Parser)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPVS anbinden (Kooperation mit Cachan?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiViews on CASL specs: CATS/viewer.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski{- This does not work due to needed ordering:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Functor Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski fmap = mapSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Monad Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski return = unitSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski m >>= k = unionManySets (setToList (fmap k m))