paulson [Fri, 16 Mar 2012 16:32:34 +0000] rev 46965
ZF news
paulson [Fri, 16 Mar 2012 16:29:51 +0000] rev 46964
merged
paulson [Fri, 16 Mar 2012 16:29:28 +0000] rev 46963
Structured transfinite induction proofs
huffman [Fri, 16 Mar 2012 15:51:53 +0100] rev 46962
make more word theorems respect int/bin distinction
wenzelm [Fri, 16 Mar 2012 18:20:12 +0100] rev 46961
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm [Fri, 16 Mar 2012 14:46:13 +0100] rev 46960
refute_params are given in *this* theory;
wenzelm [Fri, 16 Mar 2012 14:42:11 +0100] rev 46959
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm [Fri, 16 Mar 2012 13:05:30 +0100] rev 46958
define keywords early when processing the theory header, before running the body commands;
wenzelm [Fri, 16 Mar 2012 11:26:55 +0100] rev 46957
clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;
wenzelm [Thu, 15 Mar 2012 23:06:22 +0100] rev 46956
Isabelle/jEdit supports user-defined Isar commands within the running session;
wenzelm [Thu, 15 Mar 2012 22:21:28 +0100] rev 46955
merged
paulson [Thu, 15 Mar 2012 17:38:05 +0000] rev 46954
beautification and structured proofs
paulson [Thu, 15 Mar 2012 16:35:02 +0000] rev 46953
replacing ":" by "\<in>"
paulson [Thu, 15 Mar 2012 15:54:22 +0000] rev 46952
Rewrote some induction proofs to be structured
wenzelm [Thu, 15 Mar 2012 22:20:07 +0100] rev 46951
more precise TPTP keywords and dependencies;
wenzelm [Thu, 15 Mar 2012 22:08:53 +0100] rev 46950
declare command keywords via theory header, including strict checking outside Pure;
wenzelm [Thu, 15 Mar 2012 20:07:00 +0100] rev 46949
prefer formally checked @{keyword} parser;
wenzelm [Thu, 15 Mar 2012 19:48:19 +0100] rev 46948
added ML antiquotation @{keyword};
wenzelm [Thu, 15 Mar 2012 19:02:34 +0100] rev 46947
declare minor keywords via theory header;
wenzelm [Thu, 15 Mar 2012 17:45:54 +0100] rev 46946
more explicit header_edits before main text_edits;
handle reparses caused by syntax update;
wenzelm [Thu, 15 Mar 2012 17:40:26 +0100] rev 46945
declare keywords as side-effect of header edit;
parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);
wenzelm [Thu, 15 Mar 2012 14:39:42 +0100] rev 46944
more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm [Thu, 15 Mar 2012 14:22:54 +0100] rev 46943
clarified syntax of prospective keywords;
wenzelm [Thu, 15 Mar 2012 14:13:49 +0100] rev 46942
basic support for outer syntax keywords in theory header;