src/Pure/proof_general.ML
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-09-27 wenzelm 2006-09-27 Source.tty now slurps by default;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-09-20 aspinall 2006-09-20 Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
2006-08-09 wenzelm 2006-08-09 int_option: signed_string_of_int;
2006-08-02 wenzelm 2006-08-02 prems-limit: int_option;
2006-07-11 wenzelm 2006-07-11 Name.dest_skolem;
2006-06-17 wenzelm 2006-06-17 Term.skolem;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-03-21 wenzelm 2006-03-21 subtract (op =);
2006-03-14 wenzelm 2006-03-14 Output.add_mode: keyword component;
2006-02-10 wenzelm 2006-02-10 removed set quick_and_dirty and ThmDeps.enable -- no effect here;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-05 wenzelm 2006-01-05 Toplevel.proof_position_of;
2006-01-04 wenzelm 2006-01-04 adapted Toplevel.Proof;
2005-11-16 wenzelm 2005-11-16 pgmlsymbolson: append Symbol.xsymbolsN at end!
2005-11-09 wenzelm 2005-11-09 P.locale_element;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-30 aspinall 2005-09-30 Move welcomemsg and helpdoc to pgip_isar.xml
2005-09-30 aspinall 2005-09-30 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
2005-09-20 webertj 2005-09-20 undone the previous change: show_hyps not supported anymore
2005-09-20 webertj 2005-09-20 new menu item show-sort-hypotheses to toggle show_hyps
2005-09-17 wenzelm 2005-09-17 tuned comments;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update; nat_option trace_simp_depth_limit;
2005-09-15 aspinall 2005-09-15 Revert previous attribute name change, problem can be avoided in JAXB.
2005-09-15 aspinall 2005-09-15 Change PGIP attribute name class->messageclass to avoid Java keyword clash.
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-09-01 wenzelm 2005-09-01 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z; tuned;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-03 berghofe 2005-08-03 Adapted to new interface of thms_of_proof.
2005-07-29 wenzelm 2005-07-29 P.opt_locale_target;
2005-07-20 aspinall 2005-07-20 Ressurect seq attribute accidently removed
2005-07-14 haftmann 2005-07-14 (fix for smlnj)
2005-07-13 aspinall 2005-07-13 Update PGIP packet handling, fixing unique session identifier.
2005-07-13 wenzelm 2005-07-13 tuned msg;
2005-07-13 aspinall 2005-07-13 Add acceptedpgipelems message
2005-07-13 aspinall 2005-07-13 Add management for current working directory
2005-07-13 aspinall 2005-07-13 Note about theorem dependencies including themselves.
2005-07-13 aspinall 2005-07-13 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
2005-06-22 wenzelm 2005-06-22 tuned;
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 Context.theory_name; tuned;
2005-06-05 wenzelm 2005-06-05 File.platform_path;
2005-05-22 wenzelm 2005-05-22 FindTheorems.print_theorems;
2005-05-17 wenzelm 2005-05-17 var_or_skolem: always print question mark for vars stemming from skolems;
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;
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
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.
2005-03-25 aspinall 2005-03-25 Support new PGIP commands redostep, redoitem
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-27 berghofe 2005-01-27 Added show_var_qmarks flag.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-12-13 aspinall 2004-12-13 Fix pgmlsymbolson/off.
2004-12-10 aspinall 2004-12-10 Support PGIP <whitespace>, <dostep>, <doitem> elements as input
2004-12-10 aspinall 2004-12-10 Insert pgmltext element into responses in PGIP mode