Thu, 30 Aug 2012 15:44:03 +0900 Christian Sternagel forgot to add lemmas
Thu, 30 Aug 2012 13:44:15 +0900 Christian Sternagel hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI
Thu, 30 Aug 2012 13:39:43 +0900 Christian Sternagel reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Thu, 30 Aug 2012 13:39:30 +0900 Christian Sternagel reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Thu, 30 Aug 2012 13:38:27 +0900 Christian Sternagel added theory instantiating type class order for list prefixes
Thu, 30 Aug 2012 13:06:04 +0900 Christian Sternagel Main is implicitly imported via Sublist
Thu, 30 Aug 2012 13:05:11 +0900 Christian Sternagel added author
Thu, 30 Aug 2012 13:03:03 +0900 Christian Sternagel List is implicitly imported by Main
Wed, 29 Aug 2012 16:25:35 +0900 Christian Sternagel introduced "sub" as abbreviation for "emb (op =)";
Wed, 29 Aug 2012 12:24:26 +0900 Christian Sternagel base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
Wed, 29 Aug 2012 12:23:14 +0900 Christian Sternagel dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
Wed, 29 Aug 2012 11:05:44 +0900 Christian Sternagel more lemmas on suffixes and embedding
Wed, 29 Aug 2012 10:57:24 +0900 Christian Sternagel changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
Wed, 29 Aug 2012 10:48:28 +0900 Christian Sternagel added embedding for lists (constant emb)
Wed, 29 Aug 2012 10:46:11 +0900 Christian Sternagel renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=
Wed, 29 Aug 2012 10:35:05 +0900 Christian Sternagel renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix
Wed, 29 Aug 2012 10:27:56 +0900 Christian Sternagel renamed theory List_Prefix into Sublist (since it is not only about prefixes)
Mon, 03 Sep 2012 11:54:21 +0200 blanchet compile
Mon, 03 Sep 2012 11:54:21 +0200 blanchet rearrange dependencies
Mon, 03 Sep 2012 11:54:21 +0200 blanchet renamed three BNF/(co)datatype-related commands
Mon, 03 Sep 2012 11:30:29 +0200 wenzelm tuned boundary cases of command-line;
Mon, 03 Sep 2012 11:09:25 +0200 wenzelm "isabelle logo" produces EPS and PDF format simultaneously;
Mon, 03 Sep 2012 10:17:17 +0200 wenzelm actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
Mon, 03 Sep 2012 09:15:58 +0200 wenzelm tuned proofs;
Mon, 03 Sep 2012 09:15:40 +0200 wenzelm some parallel ML;
Sun, 02 Sep 2012 21:24:33 +0200 wenzelm proper classpath on windows;
Sun, 02 Sep 2012 21:07:50 +0200 wenzelm proper classpath for Java FX;
Sun, 02 Sep 2012 21:01:11 +0200 wenzelm basic setup for HTML5 panel;
Sun, 02 Sep 2012 19:26:05 +0200 wenzelm basic support for Java FX;
Sun, 02 Sep 2012 14:02:05 +0200 wenzelm maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
Sat, 01 Sep 2012 19:46:21 +0200 wenzelm removed unused material;
Sat, 01 Sep 2012 19:43:18 +0200 wenzelm discontinued complicated/unreliable notion of recent proofs within context;
Sat, 01 Sep 2012 19:27:28 +0200 wenzelm central management of forked goals wrt. transaction id;
Fri, 31 Aug 2012 22:34:37 +0200 wenzelm merged
Fri, 31 Aug 2012 22:25:06 +0200 wenzelm always register proofs, even for empty binding;
Fri, 31 Aug 2012 22:24:14 +0200 wenzelm tuned signature;
Fri, 31 Aug 2012 16:07:06 +0200 blanchet made parser a bit more flexible
Fri, 31 Aug 2012 16:07:06 +0200 blanchet tuning
Fri, 31 Aug 2012 16:07:06 +0200 blanchet pad the selectors' list with default names
Fri, 31 Aug 2012 16:07:06 +0200 blanchet generate default names for selectors
Fri, 31 Aug 2012 15:04:03 +0200 blanchet renamed "disc_disjoint" property "disj_exclus"
Fri, 31 Aug 2012 15:04:03 +0200 blanchet optimized "mk_split_tac" + use "notes"
Fri, 31 Aug 2012 15:04:03 +0200 blanchet optimized "mk_case_disc_tac" further
Fri, 31 Aug 2012 15:04:03 +0200 blanchet optimized "mk_case_disc_tac"
Fri, 31 Aug 2012 15:04:03 +0200 blanchet tuning
Fri, 31 Aug 2012 15:04:03 +0200 blanchet rationalized data structure for distinctness theorems
Fri, 31 Aug 2012 15:04:03 +0200 blanchet optimized "case_cong" proof
Fri, 31 Aug 2012 15:04:03 +0200 blanchet allow default names for selectors via wildcard (_) + fix wrong index (k)
Fri, 31 Aug 2012 15:04:03 +0200 blanchet minor fixes (for compatibility with existing datatype package)
Fri, 31 Aug 2012 15:04:03 +0200 blanchet generate "split_asm" property
Fri, 31 Aug 2012 15:04:03 +0200 blanchet generate "split" property
Fri, 31 Aug 2012 16:35:30 +0200 wenzelm more precise register_proofs for local goals;
Fri, 31 Aug 2012 15:25:26 +0200 wenzelm more informative error message from failed goal forks (violating old-style TTY protocol!);
Fri, 31 Aug 2012 15:24:26 +0200 wenzelm avoid empty tooltips;
Fri, 31 Aug 2012 15:03:44 +0200 wenzelm clarified command status (again);
Fri, 31 Aug 2012 14:52:29 +0200 wenzelm recovered ScrollPane from d899be1cfe6d;
Fri, 31 Aug 2012 14:35:04 +0200 wenzelm more markup for failed goal forks, reusing "bad";
Fri, 31 Aug 2012 13:23:25 +0200 wenzelm further refinement of command status, to accomodate forked proofs;
Thu, 30 Aug 2012 22:38:12 +0200 wenzelm merged;
Thu, 30 Aug 2012 17:22:34 +0200 blanchet make parallel list indexing possible for inject theorems
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip