src/Pure/proof_general.ML
Wed, 13 Jul 2005 16:08:21 +0200 wenzelm tuned msg;
Wed, 13 Jul 2005 15:25:05 +0200 aspinall Add acceptedpgipelems message
Wed, 13 Jul 2005 12:14:23 +0200 aspinall Add management for current working directory
Wed, 13 Jul 2005 11:29:08 +0200 aspinall Note about theorem dependencies including themselves.
Wed, 13 Jul 2005 11:28:09 +0200 aspinall Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
Wed, 22 Jun 2005 19:41:19 +0200 wenzelm tuned;
Mon, 20 Jun 2005 22:13:59 +0200 wenzelm get_thm(s): Name;
Fri, 17 Jun 2005 18:33:25 +0200 wenzelm Context.theory_name;
Sun, 05 Jun 2005 11:31:22 +0200 wenzelm File.platform_path;
Sun, 22 May 2005 16:51:10 +0200 wenzelm FindTheorems.print_theorems;
Tue, 17 May 2005 18:51:16 +0200 wenzelm var_or_skolem: always print question mark for vars stemming from skolems;
Tue, 17 May 2005 18:10:38 +0200 wenzelm renamed show_var_qmarks to show_question_marks;
Mon, 16 May 2005 09:35:05 +0200 kleing searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy;
Fri, 25 Mar 2005 17:47:11 +0100 aspinall Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
Fri, 25 Mar 2005 14:04:42 +0100 aspinall Support new PGIP commands redostep, redoitem
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Thu, 27 Jan 2005 12:34:09 +0100 berghofe Added show_var_qmarks flag.
Mon, 24 Jan 2005 17:59:48 +0100 berghofe Adapted to modified interface of PureThy.get_thm(s).
Mon, 13 Dec 2004 14:31:02 +0100 aspinall Fix pgmlsymbolson/off.
Fri, 10 Dec 2004 22:33:16 +0100 aspinall Support PGIP <whitespace>, <dostep>, <doitem> elements as input
Fri, 10 Dec 2004 22:25:31 +0100 aspinall Insert pgmltext element into responses in PGIP mode
Tue, 16 Nov 2004 20:20:14 +0100 aspinall Markup obtain as introducing a nested goal.
Mon, 15 Nov 2004 13:51:43 +0100 aspinall Add <undoitem> for theory-state undos.
Thu, 28 Oct 2004 17:11:51 +0200 aspinall Make <undostep> call undos_proof to display resulting proofstate.
Wed, 27 Oct 2004 19:45:16 +0200 aspinall Revert change to pgml_sym
Sun, 24 Oct 2004 15:41:52 +0200 aspinall Simplification to symbol processing; put quotes around theory name in message.
Thu, 21 Oct 2004 19:21:32 +0200 aspinall Fix <closetheory>
Mon, 11 Oct 2004 10:52:18 +0200 berghofe Added entry in Settings menu for Toplevel.skip_proofs flag.
Sat, 02 Oct 2004 19:22:16 +0200 aspinall Add openblock/closeblock to other opengoal/closegoal elements
Fri, 01 Oct 2004 11:51:55 +0200 aspinall Comments
Tue, 28 Sep 2004 10:44:19 +0200 aspinall Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
Mon, 27 Sep 2004 16:03:16 +0200 aspinall Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
Wed, 08 Sep 2004 21:57:19 +0200 aspinall Tweak parentnames attribute on opentheory
Wed, 08 Sep 2004 21:48:10 +0200 aspinall Support parsing of -- {* comments *}. Add extra output channels.
Fri, 03 Sep 2004 00:26:18 +0200 aspinall Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
Mon, 23 Aug 2004 18:31:18 +0200 berghofe Adapted to new interface of function ThyLoad.check_file
Thu, 19 Aug 2004 01:20:17 +0200 aspinall Add systemcmd.
Thu, 19 Aug 2004 00:47:15 +0200 aspinall Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
Wed, 18 Aug 2004 16:25:27 +0200 aspinall Version for PGIP 2.X, with greatly improved parsing and XML handling.
Mon, 16 Aug 2004 18:05:41 +0200 aspinall Experimental version supporting PGIP, merged with main branch with help from Makarius.
Tue, 29 Jun 2004 11:18:34 +0200 kleing license change to BSD
Tue, 22 Jun 2004 09:51:23 +0200 wenzelm tuned output;
Sun, 20 Jun 2004 09:26:48 +0200 wenzelm Symbol.encode_raw;
Wed, 09 Jun 2004 18:54:07 +0200 wenzelm Path.split_ext; more robust inform_file_processed;
Sun, 06 Jun 2004 18:35:26 +0200 wenzelm Symbol.output;
Sat, 29 May 2004 15:02:35 +0200 wenzelm Output.add_mode; Output.timing;
Mon, 10 May 2004 19:25:42 +0200 wenzelm ProofGeneral.process_pgip command;
Thu, 06 May 2004 14:17:07 +0200 wenzelm show_structs option;
Mon, 26 Apr 2004 14:57:30 +0200 wenzelm removed obsolete 'undo';
Thu, 15 Apr 2004 13:04:50 +0200 nipkow "haspref" -> "oldhaspref" (David Aspinall)
Thu, 15 Apr 2004 09:33:12 +0200 schirmer bugfix in xsymbols_output
Wed, 14 Apr 2004 15:09:51 +0200 nipkow corrected PG url in comment
Wed, 14 Apr 2004 12:19:16 +0200 schirmer * raw control symbols are of the form \<^raw:...> now.
Tue, 13 Apr 2004 23:08:12 +0200 schirmer * cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
Tue, 25 Mar 2003 10:03:11 +0100 berghofe Added show_brackets to settings menu.
Mon, 03 Feb 2003 11:07:09 +0100 berghofe Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
Wed, 27 Nov 2002 17:16:47 +0100 berghofe Added some functions for processing PGIP (thanks to David Aspinall).
Mon, 14 Oct 2002 10:44:32 +0200 nipkow Ported find_intro/elim to Isar.
less more (0) -60 tip