Thu, 28 Oct 2004 17:11:51 +0200 |
aspinall |
Make <undostep> call undos_proof to display resulting proofstate.
|
file |
diff |
annotate
|
Wed, 27 Oct 2004 19:45:16 +0200 |
aspinall |
Revert change to pgml_sym
|
file |
diff |
annotate
|
Sun, 24 Oct 2004 15:41:52 +0200 |
aspinall |
Simplification to symbol processing; put quotes around theory name in message.
|
file |
diff |
annotate
|
Thu, 21 Oct 2004 19:21:32 +0200 |
aspinall |
Fix <closetheory>
|
file |
diff |
annotate
|
Mon, 11 Oct 2004 10:52:18 +0200 |
berghofe |
Added entry in Settings menu for Toplevel.skip_proofs flag.
|
file |
diff |
annotate
|
Sat, 02 Oct 2004 19:22:16 +0200 |
aspinall |
Add openblock/closeblock to other opengoal/closegoal elements
|
file |
diff |
annotate
|
Fri, 01 Oct 2004 11:51:55 +0200 |
aspinall |
Comments
|
file |
diff |
annotate
|
Tue, 28 Sep 2004 10:44:19 +0200 |
aspinall |
Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
|
file |
diff |
annotate
|
Mon, 27 Sep 2004 16:03:16 +0200 |
aspinall |
Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
|
file |
diff |
annotate
|
Wed, 08 Sep 2004 21:57:19 +0200 |
aspinall |
Tweak parentnames attribute on opentheory
|
file |
diff |
annotate
|
Wed, 08 Sep 2004 21:48:10 +0200 |
aspinall |
Support parsing of -- {* comments *}. Add extra output channels.
|
file |
diff |
annotate
|
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.
|
file |
diff |
annotate
|
Mon, 23 Aug 2004 18:31:18 +0200 |
berghofe |
Adapted to new interface of function ThyLoad.check_file
|
file |
diff |
annotate
|
Thu, 19 Aug 2004 01:20:17 +0200 |
aspinall |
Add systemcmd.
|
file |
diff |
annotate
|
Thu, 19 Aug 2004 00:47:15 +0200 |
aspinall |
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
|
file |
diff |
annotate
|
Wed, 18 Aug 2004 16:25:27 +0200 |
aspinall |
Version for PGIP 2.X, with greatly improved parsing and XML handling.
|
file |
diff |
annotate
|
Mon, 16 Aug 2004 18:05:41 +0200 |
aspinall |
Experimental version supporting PGIP, merged with main branch with help from Makarius.
|
file |
diff |
annotate
|
Tue, 29 Jun 2004 11:18:34 +0200 |
kleing |
license change to BSD
|
file |
diff |
annotate
|
Tue, 22 Jun 2004 09:51:23 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
Sun, 20 Jun 2004 09:26:48 +0200 |
wenzelm |
Symbol.encode_raw;
|
file |
diff |
annotate
|
Wed, 09 Jun 2004 18:54:07 +0200 |
wenzelm |
Path.split_ext; more robust inform_file_processed;
|
file |
diff |
annotate
|
Sun, 06 Jun 2004 18:35:26 +0200 |
wenzelm |
Symbol.output;
|
file |
diff |
annotate
|
Sat, 29 May 2004 15:02:35 +0200 |
wenzelm |
Output.add_mode; Output.timing;
|
file |
diff |
annotate
|
Mon, 10 May 2004 19:25:42 +0200 |
wenzelm |
ProofGeneral.process_pgip command;
|
file |
diff |
annotate
|
Thu, 06 May 2004 14:17:07 +0200 |
wenzelm |
show_structs option;
|
file |
diff |
annotate
|
Mon, 26 Apr 2004 14:57:30 +0200 |
wenzelm |
removed obsolete 'undo';
|
file |
diff |
annotate
|
Thu, 15 Apr 2004 13:04:50 +0200 |
nipkow |
"haspref" -> "oldhaspref" (David Aspinall)
|
file |
diff |
annotate
|
Thu, 15 Apr 2004 09:33:12 +0200 |
schirmer |
bugfix in xsymbols_output
|
file |
diff |
annotate
|
Wed, 14 Apr 2004 15:09:51 +0200 |
nipkow |
corrected PG url in comment
|
file |
diff |
annotate
|
Wed, 14 Apr 2004 12:19:16 +0200 |
schirmer |
* raw control symbols are of the form \<^raw:...> now.
|
file |
diff |
annotate
|
Tue, 13 Apr 2004 23:08:12 +0200 |
schirmer |
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
|
file |
diff |
annotate
|
Tue, 25 Mar 2003 10:03:11 +0100 |
berghofe |
Added show_brackets to settings menu.
|
file |
diff |
annotate
|
Mon, 03 Feb 2003 11:07:09 +0100 |
berghofe |
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
|
file |
diff |
annotate
|
Wed, 27 Nov 2002 17:16:47 +0100 |
berghofe |
Added some functions for processing PGIP (thanks to David Aspinall).
|
file |
diff |
annotate
|
Mon, 14 Oct 2002 10:44:32 +0200 |
nipkow |
Ported find_intro/elim to Isar.
|
file |
diff |
annotate
|
Wed, 28 Aug 2002 15:27:43 +0200 |
wenzelm |
improved tell_thm_deps;
|
file |
diff |
annotate
|
Tue, 27 Aug 2002 15:40:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 27 Aug 2002 11:04:27 +0200 |
wenzelm |
result dependency output;
|
file |
diff |
annotate
|
Thu, 18 Jul 2002 12:09:08 +0200 |
wenzelm |
fixed inform_file_retracted: remove_thy;
|
file |
diff |
annotate
|
Tue, 02 Jul 2002 17:44:13 +0200 |
wenzelm |
thms_containing: optional limit argument;
|
file |
diff |
annotate
|
Tue, 02 Jul 2002 15:38:13 +0200 |
wenzelm |
ProofContext.print_thms_containing;
|
file |
diff |
annotate
|
Mon, 21 Jan 2002 22:27:34 +0100 |
wenzelm |
full_proofs;
|
file |
diff |
annotate
|
Wed, 16 Jan 2002 21:01:08 +0100 |
wenzelm |
tuned title;
|
file |
diff |
annotate
|
Wed, 16 Jan 2002 20:57:02 +0100 |
wenzelm |
Interface/proof_general.ML move to proof_general.ML;
|
file |
diff |
annotate
|