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 |
2857cf346f2387af92b04a43c41e829c00664ed1 |
|
20-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
port to Isabelle2014 |
575b1f7dfc583b5cb1d7d2f28c662e72642cd230 |
|
14-Jan-2014 |
Christian Maeder <Christian.Maeder@dfki.de> |
revert spechub/Hets@0fc370b28679137dec18ed4263e7e774a9c952cd and continue working with Isabelle2012
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18438 cec4b9c1-7d33-0410-9eda-942365e851bb |
0fc370b28679137dec18ed4263e7e774a9c952cd |
|
13-Jan-2014 |
Christian Maeder <Christian.Maeder@dfki.de> |
adjusted to Isabelle 2013-2 wrt uses keyword
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18434 cec4b9c1-7d33-0410-9eda-942365e851bb |
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 |
80fa8cedf41af85cd602945b6a267242f44a7b81 |
|
22-Oct-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
removed ghc warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18275 cec4b9c1-7d33-0410-9eda-942365e851bb |
4259e185f367aa660369432548aae92f9d828bde |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved export of definitions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18272 cec4b9c1-7d33-0410-9eda-942365e851bb |
5d127223138daa49b62042a4f10fb8e738a41ffb |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed small pretty printer bug
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18271 cec4b9c1-7d33-0410-9eda-942365e851bb |
8a5f04e1494456d1270f272db0890c327797f05e |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
pretty print primrec, fixrec, domain
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18265 cec4b9c1-7d33-0410-9eda-942365e851bb |
5e4fe646cad79449dff25a3bb7fcebad76b72c95 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
* use HOLCF image
* export / import HOLCF commands domain and fixrec
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18264 cec4b9c1-7d33-0410-9eda-942365e851bb |
10598b3b999ecbac0347ff422d56b1d97db296b7 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
* export param type inferred from context
* further improvements
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18263 cec4b9c1-7d33-0410-9eda-942365e851bb |
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
adapted import and pretty printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18262 cec4b9c1-7d33-0410-9eda-942365e851bb |
3908a6d2446de764eae4228589d19f08de1bd103 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
print fun
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18260 cec4b9c1-7d33-0410-9eda-942365e851bb |
e604ebb440d3ed0414aa2d54ff962768f0a27933 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
export and import defs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18258 cec4b9c1-7d33-0410-9eda-942365e851bb |
d40eeef0175161a089443ba027dcb635ed11a1bd |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
import and pretty print typedef
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18257 cec4b9c1-7d33-0410-9eda-942365e851bb |
93cd42c036c9ef3fed58d4872bab5d72371d80d1 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved export of subclass cmd
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18253 cec4b9c1-7d33-0410-9eda-942365e851bb |
59bed9a19a4646b44b7e837f5f9ab35183833d3b |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
import / pretty printing of instances
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18251 cec4b9c1-7d33-0410-9eda-942365e851bb |
383d883a81d3bc4ad7b14aa28e03f0f35baec458 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
adapted dtd and import
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18241 cec4b9c1-7d33-0410-9eda-942365e851bb |
61d26ef772466529400bc460e7c69f67c1173b56 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
refactored use of fixes and assumes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18234 cec4b9c1-7d33-0410-9eda-942365e851bb |
42b0311155dd27a5f8ba917b280c9f7989b73ec9 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved pretty printing of lemmas
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18233 cec4b9c1-7d33-0410-9eda-942365e851bb |
ca8f01a2b83fbb929aaf29629f71b10fd867956a |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
adapted dtd & isabelle import
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18232 cec4b9c1-7d33-0410-9eda-942365e851bb |
eca83bf7d98670ee4fa52661d2f8222429a4f91a |
|
27-Mar-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
read in function definitions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17835 cec4b9c1-7d33-0410-9eda-942365e851bb |
705d8c3d5549a00d4b00e0cb80e3a77441f85267 |
|
27-Mar-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
import of definitions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17834 cec4b9c1-7d33-0410-9eda-942365e851bb |
1bd563a2040525e10f6d1ce12f6701ebeed70668 |
|
25-Sep-2012 |
Christian Maeder <Christian.Maeder@dfki.de> |
used and docs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17421 cec4b9c1-7d33-0410-9eda-942365e851bb |
ad3ebaa39d875ef0069f3b8084c8a17432073cf9 |
|
25-Sep-2012 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17420 cec4b9c1-7d33-0410-9eda-942365e851bb |
622752e655865004756e41d39f110209dca367d0 |
|
25-Sep-2012 |
Christian Maeder <Christian.Maeder@dfki.de> |
used axiomatization instead of axioms #1063
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17419 cec4b9c1-7d33-0410-9eda-942365e851bb |
153d2d8931968e86ced679540ebc5e583e425af3 |
|
21-Sep-2012 |
Christian Maeder <Christian.Maeder@dfki.de> |
paren right associative ops properly
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17397 cec4b9c1-7d33-0410-9eda-942365e851bb |
05981c85bdffd48b8ba376e46e2ca4a4b5822387 |
|
19-Sep-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
add automatic proofs to theorems in the context of locales
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17368 cec4b9c1-7d33-0410-9eda-942365e851bb |
88742725989560e29a45dcef33ebd87e97e5f967 |
|
19-Sep-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed a couple issues with the pretty printer
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17367 cec4b9c1-7d33-0410-9eda-942365e851bb |
546dccb1b9812ac3c29be6052dafde2c9de0db3c |
|
19-Sep-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
print fixes before assumptions so that they are not erroneously declared as variables
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17366 cec4b9c1-7d33-0410-9eda-942365e851bb |
62d292e9e9227b10af78c78c6f11074e0d4b0d99 |
|
07-Aug-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
first support for importing locales from isabelle
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17140 cec4b9c1-7d33-0410-9eda-942365e851bb |
85078a17c8b15bdab3e3ccae95449eff7660e4a8 |
|
04-Jul-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
do not display consts for primrecs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17009 cec4b9c1-7d33-0410-9eda-942365e851bb |
50ec2512ec38a3a0c793c65583e60ef12beaae33 |
|
04-Jul-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
eliminated RecDef as its use resulted in invalid isabelle 2012 code
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17008 cec4b9c1-7d33-0410-9eda-942365e851bb |
4e46dc76096a52122603f8c2aeae1c508313ae74 |
|
04-Jul-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
do not print any form of type as superclass
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17007 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 |
bbd8611625672f9338ef6d26ee98abab4a939895 |
|
28-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
reintroduced orderCDecs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16990 cec4b9c1-7d33-0410-9eda-942365e851bb |
d7918e24c4f5cbb4adfe36c02da28014bfdc9492 |
|
28-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved pretty printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16989 cec4b9c1-7d33-0410-9eda-942365e851bb |
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34 |
|
28-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
added support for importing classes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16988 cec4b9c1-7d33-0410-9eda-942365e851bb |
952051448ecc60de5f22f778ee60c16c781ab114 |
|
12-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed naming of bound variables
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16914 cec4b9c1-7d33-0410-9eda-942365e851bb |
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daae |
|
12-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed problems related to type variables
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16906 cec4b9c1-7d33-0410-9eda-942365e851bb |
b538e214277386123cb6f1ab0c99ae8fd3a03963 |
|
12-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
Added (rudimentary) pretty printing support for isabelle imports (only infix)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16905 cec4b9c1-7d33-0410-9eda-942365e851bb |
547a7a7094b5657eaf5a7ca89840cebc83b09d0f |
|
12-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
added bound variables
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16904 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 |
1c6f55a3e6d9f7d2d1ba1edf96e26d3cf5e0d99a |
|
15-Mar-2012 |
Christian Maeder <Christian.Maeder@dfki.de> |
quote data type strings containing spaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16728 cec4b9c1-7d33-0410-9eda-942365e851bb |
22b772f8753f0cdb4508ba460356c238de2ee375 |
|
14-Mar-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
first version of import from isabelle. has issues with printing imported datatypes and doesn't support all term types yet
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16726 cec4b9c1-7d33-0410-9eda-942365e851bb |
80f5899bc42f833b3ed367d63d6151fa7e3c5ccb |
|
28-Nov-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
fixed #976 builtin type names
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16493 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 |
db65acd12aad9d2864fd551782e92e42bd6dbf29 |
|
10-Feb-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
Isabelle 2011 expects .ML extension
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14513 cec4b9c1-7d33-0410-9eda-942365e851bb |
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853b |
|
02-Feb-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
properly top sort Isabelle domain tables
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14467 cec4b9c1-7d33-0410-9eda-942365e851bb |
7a760fce86044af4d2998c956b2b4dd29115df99 |
|
01-Feb-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up and used sortBy
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14466 cec4b9c1-7d33-0410-9eda-942365e851bb |
91084541005fb26556f5dfcda3592cbd7168c351 |
|
01-Feb-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
indexed type variables are not used
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14465 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 |
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 |
e79249c976eff391999c5caebd171bededc26e33 |
|
24-Mar-2010 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Added a new sentence type to represent a colelction of lemmas
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13270 cec4b9c1-7d33-0410-9eda-942365e851bb |
5b651cd8e9e17d8d924ab22cc4fc927cd8634a14 |
|
21-Jan-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
do not change header
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12992 cec4b9c1-7d33-0410-9eda-942365e851bb |
0a07bd14fe2814f7514ab02239c06a3f6851f7b7 |
|
20-Jan-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
create Isabelle2009 code
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12987 cec4b9c1-7d33-0410-9eda-942365e851bb |
24d85869005a9175634792b34d2234c0a63215cb |
|
01-Sep-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
do not assume HETS_LIB to be a directory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12378 cec4b9c1-7d33-0410-9eda-942365e851bb |
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3e |
|
27-Aug-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored using Common.Utils.number
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12314 cec4b9c1-7d33-0410-9eda-942365e851bb |
a36744e684c99272f0ec7e6d3cfb7e38a20d385f |
|
31-Jul-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
output the projection function with its profile
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12019 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 |
46ed65e4c2913e0cf1bf84e9363685bd932b04c9 |
|
05-Mar-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
export printTerm
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11491 cec4b9c1-7d33-0410-9eda-942365e851bb |
c9936ad4129f3a3b40f426b7f3440e6c8fc37899 |
|
13-Jan-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
print additional imports #639
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11255 cec4b9c1-7d33-0410-9eda-942365e851bb |
36a612da157c0b6528b87533da53ec7e62bdf5d7 |
|
22-Aug-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Added the generation of the choose functions along with the theorem and
proof in the comorphism CspCASL2IsabelleHOL.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10574 cec4b9c1-7d33-0410-9eda-942365e851bb |
85335fd0f0b212c7c3e097d94dfcccb2bdffa4e7 |
|
21-Aug-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Added to the comorphism CspCASL2Isabelle the generation of Bar Types,
and Alphabet type (type synonym).
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10560 cec4b9c1-7d33-0410-9eda-942365e851bb |
1c6a73b4e0667c9397ef40a017ea18335489b70b |
|
20-Aug-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Added two new proof methods for Isabelle proofs (auto and simp with
modifiers). Added modifiers as a datatype. chanaged proofs methods to
use terms and not strings. Finished the decomposition proof generation
for the translation CspCASL2IsabelleHOL
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10548 cec4b9c1-7d33-0410-9eda-942365e851bb |
fb571b4492d58282a9cf249cd015084c13d141c0 |
|
19-Aug-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Merged Isabelle.ProofPrint and Isabelle.Print
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10541 cec4b9c1-7d33-0410-9eda-942365e851bb |
01e278bdd7dce13b9303ed3d79683d83c89d09f9 |
|
19-Aug-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
merged Isabelle.IsaSign and Isabelle.IsaProof
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10539 cec4b9c1-7d33-0410-9eda-942365e851bb |
e142361a68000c1ef88e2b072933ca68cf6d2e85 |
|
01-Aug-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
untabified
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10422 cec4b9c1-7d33-0410-9eda-942365e851bb |
e4257c7b13b1122a1e6ec9e43753f3e565b88449 |
|
29-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
started #557
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10406 cec4b9c1-7d33-0410-9eda-942365e851bb |
64a52f46226e2b2fad4306745ad27b648f381152 |
|
18-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
allow breaks in meta terms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10367 cec4b9c1-7d33-0410-9eda-942365e851bb |
c29a17786ce49013fef085be0839185abe077c22 |
|
18-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
don't use alternative syntax for refute sentences
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10366 cec4b9c1-7d33-0410-9eda-942365e851bb |
28f7b58d3c0916e7a74d811087849150b96ffc03 |
|
17-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
even more cleanup
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10354 cec4b9c1-7d33-0410-9eda-942365e851bb |
3620fbd44ccf0f115e7daee950135b7097857f31 |
|
17-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
more cleaning up
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10352 cec4b9c1-7d33-0410-9eda-942365e851bb |
055577747e0026ff8168808a7f228bb3f433b5bb |
|
17-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced some terms by known constants
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10351 cec4b9c1-7d33-0410-9eda-942365e851bb |
c962b775a1084a2013cdf23fd1e4a91a7994daa2 |
|
17-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
keep order of sentences when printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10349 cec4b9c1-7d33-0410-9eda-942365e851bb |
89873d3eb29b4ef32bfac57443cf831c8b2e0e82 |
|
16-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
fixed instances for Haskell/test/HOLCF/ex_class_hc.thy
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10336 cec4b9c1-7d33-0410-9eda-942365e851bb |
72aaab1105e454ec9f49103874cd8006dc2a358c |
|
15-Jul-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Liam: Extended IsaSign.Sentence with a new constructor TypeDef that allows
new types to be made from old types (namely subsets). Also changed an
Isabelle Senetence to use MetaTerms so that we can use [| |] ==> in
theorems in Isabelle. Made much progress on the CspCASL2Isabelle
Comorphism.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10331 cec4b9c1-7d33-0410-9eda-942365e851bb |
8171fdc5e142d2e0e5b4af8172a5ed10e0daa827 |
|
15-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
tried to insert instance sentences
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10330 cec4b9c1-7d33-0410-9eda-942365e851bb |
c4ba3e20a432419afff01558e425e00be42871d8 |
|
15-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
added instance sentences and used Proof type
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10329 cec4b9c1-7d33-0410-9eda-942365e851bb |
e562f4e0579bf7dd11f2b77f24ef94cd0dd78319 |
|
14-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
try without printArities
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10328 cec4b9c1-7d33-0410-9eda-942365e851bb |
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3a |
|
09-Jul-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
Liam: Added a basic Isabelle Proof datatype and integrated it into IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10285 cec4b9c1-7d33-0410-9eda-942365e851bb |
51a4b3542a56baa8f452bdd87dc285af20d3607b |
|
07-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused argument
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10271 cec4b9c1-7d33-0410-9eda-942365e851bb |
f794aa9c06cdd6626e541bc56584da1f9a9a5a4c |
|
30-Jun-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
added [simp] to theorems
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10228 cec4b9c1-7d33-0410-9eda-942365e851bb |
dd2fa8009476be94158bee9d67268c3825621c4c |
|
27-May-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
only output mixfix syntax if number of arguments matches exactly
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10035 cec4b9c1-7d33-0410-9eda-942365e851bb |
7f24cfbcf531436eb1e4bb84431338d3ca0b27d0 |
|
04-Mar-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
re-inserted topological sorting of datatypes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9682 cec4b9c1-7d33-0410-9eda-942365e851bb |
bddabeca5537895e21418679e13b3601b9460b33 |
|
05-Nov-2007 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
changes to type names
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9138 cec4b9c1-7d33-0410-9eda-942365e851bb |
38f8320f50c5f63965ba42e4e48f38be07c823cf |
|
02-Nov-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed trailing white space using: perl -i -ple 's/ +$_g' */*.hs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9131 cec4b9c1-7d33-0410-9eda-942365e851bb |
3b8ed4c60cde6b3fc00836e7814262c4377e8648 |
|
01-Nov-2007 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
fixed bugs in translation to HOLCF
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9127 cec4b9c1-7d33-0410-9eda-942365e851bb |
8e6bb4331923071e07324bc145863a694bea52ce |
|
08-Oct-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
filter true lemmas when they are generated
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9002 cec4b9c1-7d33-0410-9eda-942365e851bb |
cd0fea9ed87cf249acb7dcef2b6d3e82f308114b |
|
25-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
allowed to generate a replacement for oops
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8902 cec4b9c1-7d33-0410-9eda-942365e851bb |
39f1a07923020496228e0577ac63aa94a91d63cb |
|
10-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
made it compile
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8820 cec4b9c1-7d33-0410-9eda-942365e851bb |
135bcb7f65991146c103e5e7599adbc49fe7359d |
|
16-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced senName with senAttr
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8627 cec4b9c1-7d33-0410-9eda-942365e851bb |
807d5fddaa5dd8924321c73400fcf875a9ed9a9c |
|
14-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
libdir is not needed for printing Isabelle theories
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8606 cec4b9c1-7d33-0410-9eda-942365e851bb |
c3d42e13d2a7c3749229498658aec34e7e4fd0a0 |
|
20-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
properly merged in Paolo's additions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8431 cec4b9c1-7d33-0410-9eda-942365e851bb |
07776cf28eb838aebc1a627e9c5ad7cc6111e50a |
|
20-Jul-2007 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
added translation of type synonims
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8428 cec4b9c1-7d33-0410-9eda-942365e851bb |
d4265647a1d92b293c75f9a50a33cfa3124ee958 |
|
17-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
added [rule_format] to axiom labels
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8391 cec4b9c1-7d33-0410-9eda-942365e851bb |
51cf48ba1fe50766587289c34d5457271f821f99 |
|
16-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
put commas between multiple type variables when printing type constructors in type decls
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8380 cec4b9c1-7d33-0410-9eda-942365e851bb |
e1f395fef7ea8b00a675a330e5461fad35158ca5 |
|
10-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
added haddock descriptions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8319 cec4b9c1-7d33-0410-9eda-942365e851bb |
3f69b6948966979163bdfe8331c38833d5d90ecd |
|
05-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed my maintainer email
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8261 cec4b9c1-7d33-0410-9eda-942365e851bb |
414ba142984767c4761715ff7261a139d7e2a35e |
|
14-Jun-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
only leave blanks between parens and bar
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8038 cec4b9c1-7d33-0410-9eda-942365e851bb |
93fdeeb31e1be4447699109f3fd1f371d6c8c8e3 |
|
13-Jun-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
leave blanks before and after a vertical bar in replaceUnderlines
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8031 cec4b9c1-7d33-0410-9eda-942365e851bb |
fe2c332c39a7d10896773cf8ae2a858751df41a5 |
|
28-May-2007 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
changes to printNInstance relative to built-in type instances
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7944 cec4b9c1-7d33-0410-9eda-942365e851bb |
86b6d1603911445e12768984ed6d20dc090795f8 |
|
25-May-2007 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
Changes to printInstance - related to translation of monads with AWE
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7939 cec4b9c1-7d33-0410-9eda-942365e851bb |
61091743da1a9ed6dfd5e077fdcc972553358962 |
|
04-Apr-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
generalized Named to SenAttr to be useable by Logic.Prover as well
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7784 cec4b9c1-7d33-0410-9eda-942365e851bb |
ad270004874ce1d0697fb30d7309f180553bb315 |
|
21-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
switched to Data.Set, Data.Map and Data.Dynamic
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7491 cec4b9c1-7d33-0410-9eda-942365e851bb |
5cfeedad8c9d43f62f8e8b85ab73c0dd4e91d976 |
|
20-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved remaining todos to trac
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7481 cec4b9c1-7d33-0410-9eda-942365e851bb |
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0 |
|
22-Jan-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
generated simplifier declaration instead of [simp] axiom attribute
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7326 cec4b9c1-7d33-0410-9eda-942365e851bb |
eea4921dafc41c1e2ed3782a9cdc1a2482b79efb |
|
23-Oct-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unnecessary Isabelle term constructors
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7094 cec4b9c1-7d33-0410-9eda-942365e851bb |
6bd95c9c221f78e167d357a678c60b2a55d8e818 |
|
06-Oct-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
refined printing of nested case exxpressions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7014 cec4b9c1-7d33-0410-9eda-942365e851bb |
29379037d0a2fc17c96c49bd343a3f276a5b34a6 |
|
02-Oct-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed termType of Free and Abs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6998 cec4b9c1-7d33-0410-9eda-942365e851bb |
892e7dc917adf3dd924fce2fadd9aa7fd3ef250a |
|
19-Sep-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
used parens instead of text lb and rb
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6951 cec4b9c1-7d33-0410-9eda-942365e851bb |
3c2fd9bc119be84f806ed173fea6a5661870fe60 |
|
19-Sep-2006 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
corrected HOL type annotation of recursive functions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6948 cec4b9c1-7d33-0410-9eda-942365e851bb |
81eaac399d69af15425d06b054e5d0331dbc132b |
|
25-Aug-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed MixfixApp constructor for an unique application representation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6892 cec4b9c1-7d33-0410-9eda-942365e851bb |
a63bf534ba3839dee4bbc76b30755e7d5149986c |
|
07-Aug-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
flattened nested tuples
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6782 cec4b9c1-7d33-0410-9eda-942365e851bb |
e4546debeef926f8a8b6b034ae105269de2cd817 |
|
01-Aug-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
filter out trivial sentences and ignore constructors as constants
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6756 cec4b9c1-7d33-0410-9eda-942365e851bb |
addb54340af3b3a96ef3a4cd2e0eae8f21cce733 |
|
27-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
provided for bars in terms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6730 cec4b9c1-7d33-0410-9eda-942365e851bb |
ca3a4317b88adee116c04c6b08458b5690d83209 |
|
27-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
corrected filtering of types that are given in the domain table
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6726 cec4b9c1-7d33-0410-9eda-942365e851bb |
d12de70436e416b477af9ae1bf6989f57488bf92 |
|
11-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
allowed more line breaks
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6656 cec4b9c1-7d33-0410-9eda-942365e851bb |
ae8052003e1ec7247597f034069db0939a7387e1 |
|
04-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
used sepByCommas or ppWithCommas
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6585 cec4b9c1-7d33-0410-9eda-942365e851bb |
47d6bc7bc9a708427f96be8d805f712697ad3d9e |
|
30-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
phased out PPUtils, used showDoc for showPretty, and moved instances and utilities to DocUtils
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6552 cec4b9c1-7d33-0410-9eda-942365e851bb |
e3c456d1e0b80a9d3d5d3edc3eb713da93967330 |
|
29-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6538 cec4b9c1-7d33-0410-9eda-942365e851bb |
a3acfb955e4427cde9094615b8a62623a441f8c7 |
|
23-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed PrettyPrint
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6506 cec4b9c1-7d33-0410-9eda-942365e851bb |
92642aea028852de185f686407c9e7489ea1250c |
|
14-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6447 cec4b9c1-7d33-0410-9eda-942365e851bb |
39982c927a6052fe2ebd13d4c03b2fcbae0d2f0c |
|
14-Jun-2006 |
Jian Chun Wang <wjch868@informatik.uni-bremen.de> |
change to new Doc
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6444 cec4b9c1-7d33-0410-9eda-942365e851bb |
123ce93713ddc426d2c37a5ed31dfc2b51a99cee |
|
07-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
make applications look nicer with fsep instead of hsep
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6424 cec4b9c1-7d33-0410-9eda-942365e851bb |
e42eddbc69dd31f7cd696e38f82acad678831cb7 |
|
31-May-2006 |
Jian Chun Wang <wjch868@informatik.uni-bremen.de> |
change to new Doc
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6408 cec4b9c1-7d33-0410-9eda-942365e851bb |
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04 |
|
20-Apr-2006 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
minor changes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6226 cec4b9c1-7d33-0410-9eda-942365e851bb |
6034a40f7444be44812edc9819de3b184220e4cb |
|
06-Apr-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
fixed and cleaned printMInstance
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6173 cec4b9c1-7d33-0410-9eda-942365e851bb |
c392534f82121db87fc8b638ac08a4a4ff0a34e1 |
|
06-Apr-2006 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
bug on theory morphism fixed
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6172 cec4b9c1-7d33-0410-9eda-942365e851bb |
821b2a961f8dff6bc566935532378fb07346bcbb |
|
23-Mar-2006 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
error message for monads
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6102 cec4b9c1-7d33-0410-9eda-942365e851bb |
62b04256f84128edd94c0575757332f84450bd69 |
|
03-Mar-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
used $HETS_LIB rather than evaluated libdir
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5914 cec4b9c1-7d33-0410-9eda-942365e851bb |
e7f7f922e73944a815e1fa75b667124d65ef7abf |
|
03-Mar-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
print the type for the lhs of ==
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5910 cec4b9c1-7d33-0410-9eda-942365e851bb |
012358a4a1161f01355e80708fbd5e156585d3ae |
|
31-Jan-2006 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
monad translation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5743 cec4b9c1-7d33-0410-9eda-942365e851bb |
0e78c46b6b4da7d56ad52620e5b9b4e396b229c7 |
|
20-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
simp only axioms and simplified printing IsaEq
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5547 cec4b9c1-7d33-0410-9eda-942365e851bb |
99c923311eab71a85f1dcc4785d349609c828da4 |
|
16-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
treated most Isabelle keywords
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5528 cec4b9c1-7d33-0410-9eda-942365e851bb |
4ef05f4edeb290beb89845f57156baa5298af7c4 |
|
08-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added consistency checking
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5506 cec4b9c1-7d33-0410-9eda-942365e851bb |
b6a54d7292d7a3713000847334de4316d105f40f |
|
08-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed module CreateThy
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5505 cec4b9c1-7d33-0410-9eda-942365e851bb |
60f23c9668dfef9725ed7f1e7a6f6e8eaafd9fc4 |
|
07-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed sentences
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5500 cec4b9c1-7d33-0410-9eda-942365e851bb |
c14fbdfe6120b1f03a5e251a5a1d7977989b5ea0 |
|
05-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
different printing for domains and datatypes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5494 cec4b9c1-7d33-0410-9eda-942365e851bb |
89c8609b3606fdb621eb8f987b88dc3813b5bbd5 |
|
05-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
readded Quoted
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5492 cec4b9c1-7d33-0410-9eda-942365e851bb |
c12f980ad711e880ac441cf692e8f52f79b4bafd |
|
01-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
simplified selector numbering
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5477 cec4b9c1-7d33-0410-9eda-942365e851bb |
9d34152a246db44874bd9a3c14595a9399c7cc39 |
|
30-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
print all App as MixfixApp
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5476 cec4b9c1-7d33-0410-9eda-942365e851bb |
65b218f4ca308297eb9d54cf5eeda58d71c6f856 |
|
30-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
more code reuse for if terms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5470 cec4b9c1-7d33-0410-9eda-942365e851bb |
32def3382732ed208ca04dde8a7b3a9dd3b60961 |
|
28-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
better check for theorems
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5464 cec4b9c1-7d33-0410-9eda-942365e851bb |
aa9a7405e3150b8d1caeba44af7c9e562231aff7 |
|
25-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed theory creation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5461 cec4b9c1-7d33-0410-9eda-942365e851bb |
576ccd5a62961b379f40158ad35589c90cb7758b |
|
23-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
rewrote pretty printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5447 cec4b9c1-7d33-0410-9eda-942365e851bb |
35d7afb5318df6be8f56fdcb97da58b01905d990 |
|
18-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
don't print priorities for constants
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5436 cec4b9c1-7d33-0410-9eda-942365e851bb |
547e148361d0a055c02a6195833e03dd08d5f643 |
|
17-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
show priority numbers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5414 cec4b9c1-7d33-0410-9eda-942365e851bb |
cded714319c4eed27d3562d250b1177de2f2f0cb |
|
16-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
no Show for printAlt
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5406 cec4b9c1-7d33-0410-9eda-942365e851bb |
f6a39d688e86d8b13524dc8cea1e755cd1219cc5 |
|
11-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
commented out printAlt as it does not work
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5385 cec4b9c1-7d33-0410-9eda-942365e851bb |
2f65d931e866162d39d09c43021a55314040b377 |
|
11-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed VName for alternative syntax
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5381 cec4b9c1-7d33-0410-9eda-942365e851bb |
1ac0c4de66a297fd7e345d9275f723fd83bb7bd1 |
|
10-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up and changed second VName component
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5374 cec4b9c1-7d33-0410-9eda-942365e851bb |
036037a4510ea63a81a4829ad0c11ef39b2391b0 |
|
09-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up more and moved printNamedSen
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5366 cec4b9c1-7d33-0410-9eda-942365e851bb |
613bf0ed7d98a961755408ead328687ec17f74fd |
|
09-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused code and cleaned up a bit
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5365 cec4b9c1-7d33-0410-9eda-942365e851bb |
a026c48418d48e973de230e2632b6ad91f4feb60 |
|
09-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
Quoted is not necessary
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5358 cec4b9c1-7d33-0410-9eda-942365e851bb |
bb027d3cacbd83dfec98beb38001f105e4918557 |
|
07-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
kept only single table for domain or data type
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5350 cec4b9c1-7d33-0410-9eda-942365e851bb |
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3 |
|
26-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up pretty printing of types
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5267 cec4b9c1-7d33-0410-9eda-942365e851bb |
14a3cc9512ab27e1f59f01cc23f7d9f97e2e1c4c |
|
24-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed type synonyms IName, Indexname and CName
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5241 cec4b9c1-7d33-0410-9eda-942365e851bb |
13ed13e06a5dd4aad12044ed7e7503cbe7f62990 |
|
19-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
merged in Tina's branch
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5216 cec4b9c1-7d33-0410-9eda-942365e851bb |
5f47ba5a7151e73f2540d01492b83f7e34605730 |
|
05-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
Paolo's update
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5125 cec4b9c1-7d33-0410-9eda-942365e851bb |
8b497dd89d710634c156b64212608f221feeca0d |
|
05-Jul-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
sequence infix operator ##
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4557 cec4b9c1-7d33-0410-9eda-942365e851bb |
715d833ba655d6b7abe04c4d74d5a646587a2bbf |
|
29-Jun-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
improved formatting
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4534 cec4b9c1-7d33-0410-9eda-942365e851bb |
22448641fde7298ad9d9ddb9d2e7f4801ea01689 |
|
28-Jun-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
printing of typeDecls added back
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4518 cec4b9c1-7d33-0410-9eda-942365e851bb |
48ff6e1206124a738a2110cf336ce1efa2837e5a |
|
27-Jun-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
minor correction
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4510 cec4b9c1-7d33-0410-9eda-942365e851bb |
45dbc5b3531c2efa9a557fc8dc8f4321d1b6efc5 |
|
24-Jun-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
changes in the printing of classes and instances
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4501 cec4b9c1-7d33-0410-9eda-942365e851bb |
f3a94a197960e548ecd6520bb768cb0d547457bb |
|
15-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
aligned module description for haddock-0.7
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4438 cec4b9c1-7d33-0410-9eda-942365e851bb |
97018cf5fa25b494adffd7e9b4e87320dae6bf47 |
|
15-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced Licence with License for haddock-07
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4433 cec4b9c1-7d33-0410-9eda-942365e851bb |
b4fbc96e05117839ca409f5f20f97b3ac872d1ed |
|
13-Jun-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added maintainers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4412 cec4b9c1-7d33-0410-9eda-942365e851bb |
198bfb59d0aec1ede0d614c9128262a421a18868 |
|
20-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
fix on tuples
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4312 cec4b9c1-7d33-0410-9eda-942365e851bb |
021d18f2ee4fb07bb005693321ef9e2dd888f211 |
|
20-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
minor changes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4309 cec4b9c1-7d33-0410-9eda-942365e851bb |
c0296630e58dec5207785879df6006f2b01259ae |
|
18-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
operators + - * added
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4291 cec4b9c1-7d33-0410-9eda-942365e851bb |
6ead791aefc0939d5739e6bdce3513e76f46c037 |
|
13-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
rid of a few warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4272 cec4b9c1-7d33-0410-9eda-942365e851bb |
88ece6e49930670e8fd3ee79c89a2e918d2fbd0c |
|
12-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
adapted Common.Lib.Set and Map to ghc-6.4 library version
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4263 cec4b9c1-7d33-0410-9eda-942365e851bb |
401b13c82411866e929d1cc5d6bfe7bd22c54fe9 |
|
11-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
reverting to direct bracketing of domain applications - without using precedence trees
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4259 cec4b9c1-7d33-0410-9eda-942365e851bb |
48c02857050e76660a3aeda02dcba4cc9dd051f5 |
|
10-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
domain application dealt as PrecTermTree
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4228 cec4b9c1-7d33-0410-9eda-942365e851bb |
f9d28459072c85d4ae0bc12c1d7e4f0b57f33ae1 |
|
04-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
only show lemma when flag is set and removed unused code
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4205 cec4b9c1-7d33-0410-9eda-942365e851bb |
7c75d87ef40d4e9ba4793e09d7570210a049faf1 |
|
04-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
fixed NotCont applications
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4201 cec4b9c1-7d33-0410-9eda-942365e851bb |
9211d12224eaace6045457b313b97e4ab86f2479 |
|
03-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed Isabelle sentence type
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4190 cec4b9c1-7d33-0410-9eda-942365e851bb |
4eed11f3c47a94e8908e15a0af70370ad35b3586 |
|
03-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
new version, adapted to translate Haskell into HOLCF
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4179 cec4b9c1-7d33-0410-9eda-942365e851bb |
e404133a2e2be28b886270f28b7134a0da6a7f6e |
|
28-Apr-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed translation of Isabelle strings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4154 cec4b9c1-7d33-0410-9eda-942365e851bb |
7f6b97541fdee30d62a0a3cfa58173212a6cd002 |
|
28-Apr-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
introduced an enumeration type for the Isabelle base signatures
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4151 cec4b9c1-7d33-0410-9eda-942365e851bb |
71dc1e082c62b215e3f68baedc8e458e407e72b7 |
|
18-Apr-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added missing white space
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4078 cec4b9c1-7d33-0410-9eda-942365e851bb |
7bd5754e08c0e163f96fff840189a38394f96af0 |
|
29-Mar-2005 |
Tina Kraußer <tina@krausser.net> |
showIsaT and showIsaIT are extented versions of showIsa and showIsaI which have an additional parameter for the Isabelle-theory
all occurrences of showIsa and showIsaI are substituted by the new functions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3994 cec4b9c1-7d33-0410-9eda-942365e851bb |
15a13a08bb38e270df296d52cd7c6b455e390588 |
|
09-Mar-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
removed loop fix, because it caused malfunction with most encodings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3917 cec4b9c1-7d33-0410-9eda-942365e851bb |
68c2f69423ac541f27a8096b05e882791064af9d |
|
07-Mar-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
some improvement wrt HOLCF
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3909 cec4b9c1-7d33-0410-9eda-942365e851bb |
72a80e31851373a6a01f12c7ffa1b27c8b610ea2 |
|
03-Mar-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
non-terminating showTerm clause removed
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3902 cec4b9c1-7d33-0410-9eda-942365e851bb |
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095d |
|
02-Feb-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
adapted to new IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3763 cec4b9c1-7d33-0410-9eda-942365e851bb |
d6025ee06343191f356a59704d467866afa29900 |
|
25-Jan-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
modified according to new IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3708 cec4b9c1-7d33-0410-9eda-942365e851bb |
12efb24f0ec41a06c90c8229bf55a0ad6c32863c |
|
14-Jan-2005 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Small changes.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3673 cec4b9c1-7d33-0410-9eda-942365e851bb |
d0400dda27275f866597c978882dda3fe1fbdbdf |
|
10-Jan-2005 |
Lutz Schröder <lutz.schroeder@cs.fau.de> |
changed variable in proof of case-lemma to caseVar instead of a
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3647 cec4b9c1-7d33-0410-9eda-942365e851bb |
3dd452d488fc0e5e1dcb24d7801a29c2df3ae9b9 |
|
13-Dec-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
quote underscores in mixfix syntax
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3559 cec4b9c1-7d33-0410-9eda-942365e851bb |
e293a2e5c05881b57a7cd9a4b273b67f594e047e |
|
10-Dec-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Changed IsaSign.mkTypeAppl -> Printing of typeAppls
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3546 cec4b9c1-7d33-0410-9eda-942365e851bb |
463a6b5ab2ab317e45189cb6ac3e950a3cb9a129 |
|
09-Dec-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added printing of case alternatives (they mustn't have paranthesis)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3544 cec4b9c1-7d33-0410-9eda-942365e851bb |
4c8d161489d17edf1e15f16a1fbb5638c8c61856 |
|
18-Nov-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added case-lemma construction for every declared datatype (incl. simple proof)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3445 cec4b9c1-7d33-0410-9eda-942365e851bb |
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0 |
|
15-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved Isabelle strings and utilities to IsaConsts
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3430 cec4b9c1-7d33-0410-9eda-942365e851bb |
a3acfcfbd58cc5529becffcda29f7de49f9500a7 |
|
11-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed IsaClass again
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3422 cec4b9c1-7d33-0410-9eda-942365e851bb |
8a8e8dfa317cdb486ca05d71996a27d60bf3c718 |
|
09-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
use PrettyPrint rather than Show
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3411 cec4b9c1-7d33-0410-9eda-942365e851bb |
e79472ac9f45b44b205357ff33965c36bfe6f765 |
|
09-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
separated translation from printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3406 cec4b9c1-7d33-0410-9eda-942365e851bb |
3aa908ffbf58d3eb8e2bff0d2fc1b48877a98346 |
|
08-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
quantifiers should not all become "All"
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3398 cec4b9c1-7d33-0410-9eda-942365e851bb |
410307167d116ddab45e02698eac31043619ed05 |
|
05-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
merged in Paolo's changes of IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3382 cec4b9c1-7d33-0410-9eda-942365e851bb |
7c7bde48df618f664e8c512d1dd4d52dff00483c |
|
27-Oct-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Removed conversion to meta-implications and meta-quantifiers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3332 cec4b9c1-7d33-0410-9eda-942365e851bb |
c673000621dd506e5fc7babf8ca6303b7fcefc14 |
|
21-Oct-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
adapted header
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3315 cec4b9c1-7d33-0410-9eda-942365e851bb |
8db0251c426f1f3a595be57cc02ee878c7c86e22 |
|
21-Oct-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
use a private tree
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3309 cec4b9c1-7d33-0410-9eda-942365e851bb |
52a5c49b7e6d1dbff2e298d7287282fd84002489 |
|
14-Oct-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Replaced dummyT with noType
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3250 cec4b9c1-7d33-0410-9eda-942365e851bb |
840ad39a5a571d5170e7bc4796058208502fa73f |
|
08-Oct-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added necessary term printing (because of changes in HasCASL2Isabelle)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3230 cec4b9c1-7d33-0410-9eda-942365e851bb |
b640390417b228ce441b172f6447f1ae90a24b42 |
|
07-Sep-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Printing of infixes now takes the associativity of a term into account
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3140 cec4b9c1-7d33-0410-9eda-942365e851bb |
aef2ec6fe7797a29aae26cbcbdb70e6ec0eb0f5b |
|
25-Aug-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Adapted printing.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3086 cec4b9c1-7d33-0410-9eda-942365e851bb |
1f084d62dbf8ae72357697c226cacd1973f0c03f |
|
10-Aug-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Keep old tactic scripts
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3046 cec4b9c1-7d33-0410-9eda-942365e851bb |
586af0e9490a14dd3075095692b584c652584875 |
|
10-Aug-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added sublogics to IdComorphism
Avoided !! below ==> in IsaPrint
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3040 cec4b9c1-7d33-0410-9eda-942365e851bb |
a74b97a1e9615b64664dbea33f3ac9e6e7b2f2ac |
|
09-Aug-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
outerShowTerm also for nested -->
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3027 cec4b9c1-7d33-0410-9eda-942365e851bb |
d22c8922fc1df26565573cf532e5795543990382 |
|
09-Aug-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Output outer ! and --> as \!\! and ==>
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3022 cec4b9c1-7d33-0410-9eda-942365e851bb |
14b8979b35ac1cee33368662f45077aeb6a227c5 |
|
28-Jul-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
overlapping Show (Tree PrecTerm) instance
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2990 cec4b9c1-7d33-0410-9eda-942365e851bb |
fd9bccda7205ccbf8f0353edb9c327711d0fb2cb |
|
19-Jul-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added Isar consistent datatype printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2953 cec4b9c1-7d33-0410-9eda-942365e851bb |
cac2b3a00d21ce716bf5bf557899f0c55123835e |
|
16-Jul-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Extended showType for TVars
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2948 cec4b9c1-7d33-0410-9eda-942365e851bb |
04b1add360822e86b76b0a34ee9258e439514b28 |
|
14-Jun-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added correct printing of quantifications in formulas.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2856 cec4b9c1-7d33-0410-9eda-942365e851bb |
0f2a8687ec78c69557d72accbc33fd759f922b46 |
|
07-Jun-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Removed small bug -> bracketizing of applied operations
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2833 cec4b9c1-7d33-0410-9eda-942365e851bb |
1820d25a3bb40cf625484b1fcee1752fb33a86a8 |
|
01-Jun-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Changed some printig functions. Now the produce Isabelle-readable theories.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2782 cec4b9c1-7d33-0410-9eda-942365e851bb |
1c8c2ec97ff7dee8381aca53f0fca99c01f7b32f |
|
26-May-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Changed pretty printing for terms by introducing precedence-inclined bracketing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2717 cec4b9c1-7d33-0410-9eda-942365e851bb |
6caada8926a23123aee618f61d64fe82cfd6e91e |
|
10-May-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added freeness flag to Sort_gen_ax; new transformation to Isabelle lexis
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2574 cec4b9c1-7d33-0410-9eda-942365e851bb |
2d453384452f29ab46f29c0163a830492f936512 |
|
22-Mar-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
__* empty log message __*
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2299 cec4b9c1-7d33-0410-9eda-942365e851bb |