e9458b1a7a19a63aa4c179f9ab20f4d50681c168 |
|
25-Mar-2016 |
Jens Elkner <jel+git@iws.cs.uni-magdeburg.de> |
applied utils/replaceAllHeaders.sh
- all $Header$ tokens in doc comments replaced with corresponding filename |
3d3889e0cefcdce9b3f43c53aaa201943ac2e895 |
|
29-Nov-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
removed lots of hlint warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18342 cec4b9c1-7d33-0410-9eda-942365e851bb |
90d97972167d142dde6ee8b18d9625332040261f |
|
04-Jul-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
isabelle 2012 does not support alternative type names anymore
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17003 cec4b9c1-7d33-0410-9eda-942365e851bb |
e29b8f886533643eb2b9a8601606a9f5e40cd237 |
|
11-Apr-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
alternative names for rec types
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16783 cec4b9c1-7d33-0410-9eda-942365e851bb |
16ae470521210b4f13feaa15e6de1b343a8e4e7a |
|
26-Jul-2011 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Started the process of getting CSP-CASL-Prover to work with Isabelle 2011
Added a new Isabelle sentence constructor for primitive recursion
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@15721 cec4b9c1-7d33-0410-9eda-942365e851bb |
e7ddd5495421698701a2bbc57a5b3390a11d12ca |
|
06-Jul-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
added utilities for op types with kinds
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@15457 cec4b9c1-7d33-0410-9eda-942365e851bb |
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4 |
|
06-Jul-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored CASL's op and pred maps
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@15456 cec4b9c1-7d33-0410-9eda-942365e851bb |
93e39e7c934482489378e1f60337cdc616a1de77 |
|
26-May-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved function mapSetToList
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@15023 cec4b9c1-7d33-0410-9eda-942365e851bb |
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21e |
|
18-Apr-2011 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Fully qualified process names now have a procprofile as opposed to a list of argument sorts and communication items
CSP-CASL-Prover now working with new signatures but not for overloaded process name and still produced OLD isabelle code
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14950 cec4b9c1-7d33-0410-9eda-942365e851bb |
bcd914850de931848b86d7728192a149f9c0108b |
|
05-Apr-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
embed process equations as CASL formula extension
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14851 cec4b9c1-7d33-0410-9eda-942365e851bb |
842ae753ab848a8508c4832ab64296b929167a97 |
|
17-Mar-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
extended channel map
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14736 cec4b9c1-7d33-0410-9eda-942365e851bb |
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27b |
|
14-Mar-2011 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Major update of Csp-CASL signatures, sentences and morphisms. These reflext the changes of the institution in the WADT 10 Paper.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14705 cec4b9c1-7d33-0410-9eda-942365e851bb |
6e9970ba305cf3b2dfc285e2e21f1fc03f0a3049 |
|
04-Feb-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
simplified type construction
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14491 cec4b9c1-7d33-0410-9eda-942365e851bb |
98890889ffb2e8f6f722b00e265a211f13b5a861 |
|
01-Sep-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Added see license.txt to license field
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13959 cec4b9c1-7d33-0410-9eda-942365e851bb |
b87efd3db0d2dc41615ea28669faf80fc1b48d56 |
|
11-Aug-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Changed haddock headers and inserted empty headers for the ones missing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13857 cec4b9c1-7d33-0410-9eda-942365e851bb |
7db74d99f2d2705558510202067b91aca1912f6f |
|
09-Jul-2010 |
Liam O'Reilly <csliam@swansea.ac.uk> |
CspCASLProver now translates implied process defintions as theorems which the user should prove
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13699 cec4b9c1-7d33-0410-9eda-942365e851bb |
269c98e2ccf268d3d5d19d46d3d242fad726b882 |
|
08-Jul-2010 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Changed Isabelle (and CSP-CASL-Prover) to support new Isar instantiation syntax in place of the old one
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13695 cec4b9c1-7d33-0410-9eda-942365e851bb |
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0 |
|
24-Mar-2010 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Made use of new lemmas sentence (in IsaSign) in CspCASLProver
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13272 cec4b9c1-7d33-0410-9eda-942365e851bb |
3348c9a9d620bfab82296cc7f7a8f968f79916bc |
|
09-Nov-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
fixed bug with sort name, and axiom name conversion to Isabelle where
the special characters like square brackets were not encoded properly.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12811 cec4b9c1-7d33-0410-9eda-942365e851bb |
d3b4ad111a281d125659e12d6641943f29d6b3df |
|
06-Nov-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Added Isabelle functions Image and Range. Drastically changed how the
process translation works. It now works for channels and term prefix
in a compatible way. All channel operations are now supported by
CspCASLProver. Renaming, hiding, chaos and run are still not supported.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12792 cec4b9c1-7d33-0410-9eda-942365e851bb |
9d1c91ab0fb8707aa559df83291a970349005eaf |
|
30-Oct-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Changed how the trasitivity and identity axiom names are produced, CspCASLProver should now work better for isomorphic sorts
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12763 cec4b9c1-7d33-0410-9eda-942365e851bb |
a0d4bdc81a1e0d1963d68fc6d5e4258cbdc6bd78 |
|
30-Oct-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Created functions to generate axiom names
Used these functions in CspCASLProver
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12762 cec4b9c1-7d33-0410-9eda-942365e851bb |
82a264c7fab82cbfdac781813701b1cb0bff2e4b |
|
22-Oct-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Updated CSP-CASL-Prover to use new names of embedding injectivity axioms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12695 cec4b9c1-7d33-0410-9eda-942365e851bb |
0a83f8dcd5598436966584b858313eb5efd95d5b |
|
12-Oct-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Fixed compiler warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12625 cec4b9c1-7d33-0410-9eda-942365e851bb |
33bdce26495121cdbce30331ef90a1969126a840 |
|
17-Jun-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Comitting CspCASL Implementation after a while.
Data types for CspCASLMorphisms, mapping morphisms over CspCASL
signatures and sentences. Additions to CspCASLProver where the
Isabelle generated code for channels may be incorrect with the respect
to the CspCASL semantics (will sort out soon). Some other parts of the
CspCASL Logic may also now be working.
--This line, and those below, will be ignored--
M Comorphisms/CASL2CspCASL.hs
M Comorphisms/CspCASL2Modal.hs
M Makefile
M CspCASLProver/CspCASLProver.hs
M CspCASLProver/Consts.hs
M CspCASLProver/CspProverConsts.hs
M CspCASLProver/TransProcesses.hs
M CspCASLProver/Utils.hs
M CspCASL/SignCSP.hs
M CspCASL/CspProver_Consts.hs
M CspCASL/AS_CspCASL_Process.der.hs
M CspCASL/Morphism.hs
M CspCASL/StatAnaCSP.hs
M CspCASL/SimplifySen.hs
M CspCASL/Comorphisms.hs
M CspCASL/Print_CspCASL.hs
M CspCASL/Logic_CspCASL.hs
M Isabelle/IsaConsts.hs
M Isabelle/IsaPrint.hs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11805 cec4b9c1-7d33-0410-9eda-942365e851bb |
8ed6194df1b200ba6522dfaa0c5c8d952bc3451a |
|
25-Mar-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
* Modified Isabelle Proof Commands such that the + symbol can be used to repeat
the command in Isabelle
* Changed CspCASLProver to use the above Proof Commands
* CspCASLProver now produces much more efficient code for the reflexivity,
symmetry and transitivity proofs.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11577 cec4b9c1-7d33-0410-9eda-942365e851bb |
0e51f08fb6ced8e6a9e69eb5976fcc20dbf07019 |
|
23-Feb-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Improved simplifications of CspCASL
Term and Formulae translations within processes now works correctly
Removed all warnings from my modules during compile
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11421 cec4b9c1-7d33-0410-9eda-942365e851bb |
9738b4e358f960105062839c835bb9eff3e44588 |
|
05-Feb-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
A subset of Csp Processes are now correctly translated into CspProver (Isabelle)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11367 cec4b9c1-7d33-0410-9eda-942365e851bb |
c3efd4f435e954846981cf46bca64e0485266634 |
|
27-Jan-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Converted most of the comporphism CspCASL2IsabelleHOL to the CspCASLProver
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11323 cec4b9c1-7d33-0410-9eda-942365e851bb |
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98b |
|
24-Jan-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Added a better structure to the files for CspCASLProver - fucntions are now in appropriate places such as Consts, Utils and IsabelleUtils
Produced the preAlphabet and created the "linking" between CspCASLProver's Isabelle theory files
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11314 cec4b9c1-7d33-0410-9eda-942365e851bb |
46548eacf0dd2a0a57b972632f069b51068151dd |
|
23-Jan-2009 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Finished the data encoding for CspCASLProver - just the datapart of a
CspCASL specification.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11311 cec4b9c1-7d33-0410-9eda-942365e851bb |