| da97cb224435c57d2e1acdbff1ba2727aef8c46c |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
further improvements
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18225 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 5ae58979133bc1f8c1d9e400b95fb24d5007b18d |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
refactoring
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18224 cec4b9c1-7d33-0410-9eda-942365e851bb |
| f5bd703382ad26d86ba0ad390d82a4a3e81aba74 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse notation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18223 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 3467ccbc8c4b69ead06a6b4c7516c666f9b0618e |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse interpretation + hide_const
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18222 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 39ff2c70fb322676a393422acea71fa49b3ac4cd |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse context + abbreviation
Note: Passes irrelevant parsers to parse_theory_body to avoid
a too narrow type being assigned to parse_theory_body
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18221 cec4b9c1-7d33-0410-9eda-942365e851bb |
| a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
improved parser functions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18220 cec4b9c1-7d33-0410-9eda-942365e851bb |
| f0051190a4466db48632aa2137e50a14a434caa2 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
further parser improvements
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18219 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 26a00c47de4332eaf1ed218f7bb4df92cc44c53f |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse keywords
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18218 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 5dcd4b1e4a14c450b981acc5a4895efaaa667b93 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
* improved proof parsing using grammar in isar-ref.pdf p. 277
* further small improvements
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18216 cec4b9c1-7d33-0410-9eda-942365e851bb |
| e2f6183cac38aa0c12ebb42f526d92749fba6b43 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
allow forward fact chaining before proof using by
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18215 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 11215d71075e01a34e70e0499503aac1ce4b8954 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
assumes can be anonymous
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18214 cec4b9c1-7d33-0410-9eda-942365e851bb |
| b48dcb6f74075d06b770ac905ff25f0c592e2258 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
hopefully handle proof blocks better
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18213 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 9c1fa7e08c15b47b33a070e87fc057f2e49b9270 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
parse local context of theorem / lemma
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18212 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 1b814cc172570ad1eff000a2b9c7bf638371aa59 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
refactoring and cleanup
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18211 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 045eb445945abe778eba4f86c806e6b20e957957 |
|
24-Sep-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
simple parser for isabelle outer syntax
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18210 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 617719566ec7a718fc4f601c02ca91f21ca6deb6 |
|
27-Apr-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
new isabelle export script
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17920 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 8d414479025f8311a6666d66e2e1f5dcd3093ec1 |
|
09-Apr-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
do not export theorems, axioms and consts automatically generated for quickcheck
(happens for example when importing Main instead of HOL)w
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17847 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 |
| 904f7d0f637bf9927582a9f9339458aca1db9dfb |
|
27-Mar-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
changes necessary for isabelle 2013
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17831 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0 |
|
14-Aug-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
much better (error) messages for isabelle input
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17187 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 |
| 8c38757c50d7e8f76897f7e88097a2d3acc118a0 |
|
07-Aug-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
further work on importing locales
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17138 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78 |
|
07-Aug-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
first work for locales support
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17137 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 02ef6fcc031a33d9753dda5a46e6101328b3d7c5 |
|
04-Jul-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
do not export theorems automatically generated for classes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17004 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 25b4f7a4c38ef3061268cbb8c1281f957782fdbd |
|
04-Jul-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
adapted export_helper to changes in isabelle 2012, removed generated files
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17002 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 |
| 255a89789d3d5b19f6a8c96bf6c260a96158ef6d |
|
28-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
Restructured export_helper.ML
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16987 cec4b9c1-7d33-0410-9eda-942365e851bb |
| f58f6829ef8f3f742301e457f905fd0290716212 |
|
12-Jun-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
more aggressively remove HOL.trueprop
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16916 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 |
| 795e0408f6f9ea41b58cefbca2a8bde09daba435 |
|
11-Apr-2012 |
Jonathan von Schroeder <sternkinder@gmail.com> |
basenames for term / consts in a theory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16784 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 |
| 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 |
| 75a39ac3eec18df94df1be9c71a1f6b1f94a57a4 |
|
20-Dec-2011 |
Jonathan von Schroeder <sternkinder@gmail.com> |
added xml export from isabelle
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16567 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 6516023b9db74939c0a0f79fd6cc5bc7d9bab382 |
|
20-Dec-2011 |
Jonathan von Schroeder <sternkinder@gmail.com> |
added pattern-based filtering (get_gen_theorems uses a more simple approach)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16566 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 4d4ee5ef6601170c9d419da9fe8742c506507d11 |
|
30-Aug-2011 |
Jonathan von Schroeder <sternkinder@gmail.com> |
export from isabelle
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16048 cec4b9c1-7d33-0410-9eda-942365e851bb |
| 067b7cf571968fe8e91212059da1590c2dfa741a |
|
28-Aug-2011 |
Jonathan von Schroeder <sternkinder@gmail.com> |
a few changes to exporting from isabelle
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16038 cec4b9c1-7d33-0410-9eda-942365e851bb |