Framework.hs revision 85c51e5460cc1a90375c89d1ffbac867636fe68c
eb483f2216949400bfef8f6deb5320f071445626Christian MaederDescription : syntax and analysis for adding object logics to Hets from their specification in a logical framework
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiThe folder "Framework" contains the infrastructure needed for
eb483f2216949400bfef8f6deb5320f071445626Christian Maederextending Hets with new logics which are specified in
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maedersome logical framework. Currently, this only works for LF, but
eb483f2216949400bfef8f6deb5320f071445626Christian Maederreading Isabelle and Maude definitions of logics is also
eb483f2216949400bfef8f6deb5320f071445626Christian MaederThe module "Framework.AS" gives the abstract syntax, while the
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederstatic analysis of the newly defined logics is implemented in
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskithe module "Framework.Analysis" and it relies on the methods
eb483f2216949400bfef8f6deb5320f071445626Christian Maederprovided by the instances of the class 'Logic.Logic.LogicalFramework'.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedermodule Framework where