src/Pure/proof_general.ML
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
2004-11-16 aspinall 2004-11-16 Markup obtain as introducing a nested goal.
2004-11-15 aspinall 2004-11-15 Add <undoitem> for theory-state undos.
2004-10-28 aspinall 2004-10-28 Make <undostep> call undos_proof to display resulting proofstate.
2004-10-27 aspinall 2004-10-27 Revert change to pgml_sym
2004-10-24 aspinall 2004-10-24 Simplification to symbol processing; put quotes around theory name in message.
2004-10-21 aspinall 2004-10-21 Fix <closetheory>
2004-10-11 berghofe 2004-10-11 Added entry in Settings menu for Toplevel.skip_proofs flag.
2004-10-02 aspinall 2004-10-02 Add openblock/closeblock to other opengoal/closegoal elements
2004-10-01 aspinall 2004-10-01 Comments
2004-09-28 aspinall 2004-09-28 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
2004-09-27 aspinall 2004-09-27 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
2004-09-08 aspinall 2004-09-08 Tweak parentnames attribute on opentheory
2004-09-08 aspinall 2004-09-08 Support parsing of -- {* comments *}. Add extra output channels.
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.
2004-08-23 berghofe 2004-08-23 Adapted to new interface of function ThyLoad.check_file
2004-08-19 aspinall 2004-08-19 Add systemcmd.
2004-08-19 aspinall 2004-08-19 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
2004-08-18 aspinall 2004-08-18 Version for PGIP 2.X, with greatly improved parsing and XML handling.
2004-08-16 aspinall 2004-08-16 Experimental version supporting PGIP, merged with main branch with help from Makarius.
2004-06-29 kleing 2004-06-29 license change to BSD
2004-06-22 wenzelm 2004-06-22 tuned output;
2004-06-20 wenzelm 2004-06-20 Symbol.encode_raw;
2004-06-09 wenzelm 2004-06-09 Path.split_ext; more robust inform_file_processed;
2004-06-06 wenzelm 2004-06-06 Symbol.output;
2004-05-29 wenzelm 2004-05-29 Output.add_mode; Output.timing;
2004-05-10 wenzelm 2004-05-10 ProofGeneral.process_pgip command;
2004-05-06 wenzelm 2004-05-06 show_structs option;
2004-04-26 wenzelm 2004-04-26 removed obsolete 'undo';
2004-04-15 nipkow 2004-04-15 "haspref" -> "oldhaspref" (David Aspinall)
2004-04-15 schirmer 2004-04-15 bugfix in xsymbols_output
2004-04-14 nipkow 2004-04-14 corrected PG url in comment
2004-04-14 schirmer 2004-04-14 * raw control symbols are of the form \<^raw:...> now. * again allowing symbols to begin with "\\" instead of "\" for compatibility with ML-strings of old style theory and ML-files and isa-ProofGeneral.
2004-04-13 schirmer 2004-04-13 * cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in the scanner * output functions default_output and xsymbols_output only print one "\" for symbols (to be consistent with the scanner).
2003-03-25 berghofe 2003-03-25 Added show_brackets to settings menu.
2003-02-03 berghofe 2003-02-03 Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2002-11-27 berghofe 2002-11-27 Added some functions for processing PGIP (thanks to David Aspinall).
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-08-28 wenzelm 2002-08-28 improved tell_thm_deps;
2002-08-27 wenzelm 2002-08-27 tuned;
2002-08-27 wenzelm 2002-08-27 result dependency output;
2002-07-18 wenzelm 2002-07-18 fixed inform_file_retracted: remove_thy;
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 ProofContext.print_thms_containing;
2002-01-21 wenzelm 2002-01-21 full_proofs;
2002-01-16 wenzelm 2002-01-16 tuned title;