| 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 |
| 3496342433a87c2a3ab9950e78b33ecb03f29e15 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
reimplemented export of parent theories
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18266 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 |
| b9492cbb3cc06b0d06bee92643e48c8e0f595369 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved export
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18261 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 6764d16780980d70ed80b17465e07c3bb811e28a |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved fun export
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18259 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 |
| fce31f9f7a2e653c2cc7e55efafe3a7cee585bff |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse and export typedef
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18256 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 |
| 85b227b458a885d075f3934c210c7de0cc89ccff |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed small issues with parsing and export of instance command
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18250 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 0a4b44b3c2c874af72bf50468e14db804c8285d2 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
export instantiation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18249 cec4b9c1-7d33-0410-9eda-942365e851bb |
| c2356bf325a50171577ca2ffb33cf83bcd0786b1 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved definition export (use read_free_spec instead of read_term)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18248 cec4b9c1-7d33-0410-9eda-942365e851bb |
| eacba3959b7c09945bfb0d28ca32898c4606c220 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved lemma export
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18247 cec4b9c1-7d33-0410-9eda-942365e851bb |
| b9343d2e9e7078d3261a05e7899c74bcde032a76 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved tokenizer (drop further comments)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18246 cec4b9c1-7d33-0410-9eda-942365e851bb |
| dc89cfbc150be3b6792f559f57b6e91cd7affacb |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
keep parsed class name (instance head)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18245 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 97759cc6eafaca8c6e62ae394aa28b9642a2a6d7 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed error message (would only show ? instead of the constructor)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18244 cec4b9c1-7d33-0410-9eda-942365e851bb |
| a845310274d5bcd9da2df61599fd58eaf96ded13 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
fixed small issue with proof parsing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18243 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 |
| 8c4e6fae99499cb457b3b38bf248c30ce2f95921 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
added sigdata to export of fun / primrec
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18240 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 9a527ab7e7c0247ab32162f00c9ec630eff38a88 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
refactoring
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18238 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 93e4ae9221332f59e762fd04392096af1511f6b8 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
started adding sigdata
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18237 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 |
| 6df4343f46cc159371dfa671c5943354480f4e1c |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
xml export
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18231 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 18d5da8101a438aaf8c27d7e740f835e707fc0b8 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
* fixed a small issue with parsing contexts
* keep tokens of parsed body_elements
* functions to parse partial theory source
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18230 cec4b9c1-7d33-0410-9eda-942365e851bb |
| dfe355b50888d0dea1c12713288b652741844080 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse datatypes, primrec-functions and functions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18229 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 0f62c81f3b90f151d8b5adde2f039948e2f0dc16 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
* parse theorems, proofs and diagnostic and toplevel commands
* fixed small issue with class parsing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18227 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818a |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
basic isabelle outer syntax parser adapted from Pure/Isar/isr_syn.ML
Note: does not parse proof commands and diagnostic commands (yet)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18226 cec4b9c1-7d33-0410-9eda-942365e851bb |