| 2005-10-21 |
wenzelm |
2005-10-21 |
OldGoals;
|
file | diff | annotate |
| 2005-09-30 |
aspinall |
2005-09-30 |
Move welcomemsg and helpdoc to pgip_isar.xml
|
file | diff | annotate |
| 2005-09-30 |
aspinall |
2005-09-30 |
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
|
file | diff | annotate |
| 2005-09-20 |
webertj |
2005-09-20 |
undone the previous change: show_hyps not supported anymore
|
file | diff | annotate |
| 2005-09-20 |
webertj |
2005-09-20 |
new menu item show-sort-hypotheses to toggle show_hyps
|
file | diff | annotate |
| 2005-09-17 |
wenzelm |
2005-09-17 |
tuned comments;
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
TableFun/Symtab: curried lookup and update;
nat_option trace_simp_depth_limit;
|
file | diff | annotate |
| 2005-09-15 |
aspinall |
2005-09-15 |
Revert previous attribute name change, problem can be avoided in JAXB.
|
file | diff | annotate |
| 2005-09-15 |
aspinall |
2005-09-15 |
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
|
file | diff | annotate |
| 2005-09-08 |
haftmann |
2005-09-08 |
introduces some modern-style AList operations
|
file | diff | annotate |
| 2005-09-01 |
wenzelm |
2005-09-01 |
curried_lookup/update;
|
file | diff | annotate |
| 2005-09-01 |
wenzelm |
2005-09-01 |
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
tuned;
|
file | diff | annotate |
| 2005-08-16 |
wenzelm |
2005-08-16 |
OuterKeyword;
|
file | diff | annotate |
| 2005-08-03 |
berghofe |
2005-08-03 |
Adapted to new interface of thms_of_proof.
|
file | diff | annotate |
| 2005-07-29 |
wenzelm |
2005-07-29 |
P.opt_locale_target;
|
file | diff | annotate |
| 2005-07-20 |
aspinall |
2005-07-20 |
Ressurect seq attribute accidently removed
|
file | diff | annotate |
| 2005-07-14 |
haftmann |
2005-07-14 |
(fix for smlnj)
|
file | diff | annotate |
| 2005-07-13 |
aspinall |
2005-07-13 |
Update PGIP packet handling, fixing unique session identifier.
|
file | diff | annotate |
| 2005-07-13 |
wenzelm |
2005-07-13 |
tuned msg;
|
file | diff | annotate |
| 2005-07-13 |
aspinall |
2005-07-13 |
Add acceptedpgipelems message
|
file | diff | annotate |
| 2005-07-13 |
aspinall |
2005-07-13 |
Add management for current working directory
|
file | diff | annotate |
| 2005-07-13 |
aspinall |
2005-07-13 |
Note about theorem dependencies including themselves.
|
file | diff | annotate |
| 2005-07-13 |
aspinall |
2005-07-13 |
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
|
file | diff | annotate |
| 2005-06-22 |
wenzelm |
2005-06-22 |
tuned;
|
file | diff | annotate |
| 2005-06-20 |
wenzelm |
2005-06-20 |
get_thm(s): Name;
|
file | diff | annotate |
| 2005-06-17 |
wenzelm |
2005-06-17 |
Context.theory_name;
tuned;
|
file | diff | annotate |
| 2005-06-05 |
wenzelm |
2005-06-05 |
File.platform_path;
|
file | diff | annotate |
| 2005-05-22 |
wenzelm |
2005-05-22 |
FindTheorems.print_theorems;
|
file | diff | annotate |
| 2005-05-17 |
wenzelm |
2005-05-17 |
var_or_skolem: always print question mark for vars stemming from skolems;
|
file | diff | annotate |
| 2005-05-17 |
wenzelm |
2005-05-17 |
renamed show_var_qmarks to show_question_marks;
var_or_skolem: proper treatment of show_question_marks via Syntax.read_variable;
|
file | diff | annotate |
| 2005-05-16 |
kleing |
2005-05-16 |
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
|
file | diff | annotate |
| 2005-04-21 |
wenzelm |
2005-04-21 |
superceded by Pure.thy and CPure.thy;
|
file | diff | annotate |
| 2005-03-25 |
aspinall |
2005-03-25 |
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
|
file | diff | annotate |
| 2005-03-25 |
aspinall |
2005-03-25 |
Support new PGIP commands redostep, redoitem
|
file | diff | annotate |
| 2005-03-03 |
skalberg |
2005-03-03 |
Move towards standard functions.
|
file | diff | annotate |
| 2005-02-13 |
skalberg |
2005-02-13 |
Deleted Library.option type.
|
file | diff | annotate |
| 2005-01-27 |
berghofe |
2005-01-27 |
Added show_var_qmarks flag.
|
file | diff | annotate |
| 2005-01-24 |
berghofe |
2005-01-24 |
Adapted to modified interface of PureThy.get_thm(s).
|
file | diff | annotate |
| 2004-12-13 |
aspinall |
2004-12-13 |
Fix pgmlsymbolson/off.
|
file | diff | annotate |
| 2004-12-10 |
aspinall |
2004-12-10 |
Support PGIP <whitespace>, <dostep>, <doitem> elements as input
|
file | diff | annotate |
| 2004-12-10 |
aspinall |
2004-12-10 |
Insert pgmltext element into responses in PGIP mode
|
file | diff | annotate |
| 2004-11-16 |
aspinall |
2004-11-16 |
Markup obtain as introducing a nested goal.
|
file | diff | annotate |
| 2004-11-15 |
aspinall |
2004-11-15 |
Add <undoitem> for theory-state undos.
|
file | diff | annotate |
| 2004-10-28 |
aspinall |
2004-10-28 |
Make <undostep> call undos_proof to display resulting proofstate.
|
file | diff | annotate |
| 2004-10-27 |
aspinall |
2004-10-27 |
Revert change to pgml_sym
|
file | diff | annotate |
| 2004-10-24 |
aspinall |
2004-10-24 |
Simplification to symbol processing; put quotes around theory name in message.
|
file | diff | annotate |
| 2004-10-21 |
aspinall |
2004-10-21 |
Fix <closetheory>
|
file | diff | annotate |
| 2004-10-11 |
berghofe |
2004-10-11 |
Added entry in Settings menu for Toplevel.skip_proofs flag.
|
file | diff | annotate |
| 2004-10-02 |
aspinall |
2004-10-02 |
Add openblock/closeblock to other opengoal/closegoal elements
|
file | diff | annotate |
| 2004-10-01 |
aspinall |
2004-10-01 |
Comments
|
file | diff | annotate |
| 2004-09-28 |
aspinall |
2004-09-28 |
Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
|
file | diff | annotate |
| 2004-09-27 |
aspinall |
2004-09-27 |
Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
|
file | diff | annotate |
| 2004-09-08 |
aspinall |
2004-09-08 |
Tweak parentnames attribute on opentheory
|
file | diff | annotate |
| 2004-09-08 |
aspinall |
2004-09-08 |
Support parsing of -- {* comments *}. Add extra output channels.
|
file | diff | annotate |
| 2004-09-03 |
aspinall |
2004-09-03 |
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
|
file | diff | annotate |
| 2004-08-23 |
berghofe |
2004-08-23 |
Adapted to new interface of function ThyLoad.check_file
|
file | diff | annotate |
| 2004-08-19 |
aspinall |
2004-08-19 |
Add systemcmd.
|
file | diff | annotate |
| 2004-08-19 |
aspinall |
2004-08-19 |
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
|
file | diff | annotate |
| 2004-08-18 |
aspinall |
2004-08-18 |
Version for PGIP 2.X, with greatly improved parsing and XML handling.
|
file | diff | annotate |
| 2004-08-16 |
aspinall |
2004-08-16 |
Experimental version supporting PGIP, merged with main branch with help from Makarius.
|
file | diff | annotate |