Tue, 04 Sep 2012 16:27:27 +0200 blanchet implemented "mk_half_distinct_tac"
Tue, 04 Sep 2012 16:17:22 +0200 blanchet implemented "mk_inject_tac"
Tue, 04 Sep 2012 15:51:32 +0200 blanchet implemented "mk_exhaust_tac"
Tue, 04 Sep 2012 14:21:11 +0200 blanchet more work on FP sugar
Tue, 04 Sep 2012 13:06:41 +0200 blanchet more work on sugar + simplify Trueprop + eq idiom everywhere
Tue, 04 Sep 2012 13:05:07 +0200 blanchet renamed "disc_exclus" theorem to "disc_exclude"
Tue, 04 Sep 2012 13:05:01 +0200 blanchet more work on FP sugar
Tue, 04 Sep 2012 13:02:32 +0200 blanchet smarter "*" syntax -- fallback on "_" if "*" is impossible
Tue, 04 Sep 2012 13:02:32 +0200 blanchet more work on FP sugar
Tue, 04 Sep 2012 13:02:31 +0200 blanchet renamed theorem
Tue, 04 Sep 2012 13:02:30 +0200 blanchet tuned TODO comment
Tue, 04 Sep 2012 13:02:30 +0200 blanchet allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
Tue, 04 Sep 2012 13:02:29 +0200 blanchet removed oddities
Tue, 04 Sep 2012 13:02:28 +0200 blanchet allow "*" to indicate no discriminator
Tue, 04 Sep 2012 13:02:28 +0200 blanchet tuned TODOs
Tue, 04 Sep 2012 13:02:26 +0200 blanchet started work on sugared "(co)data" commands
Tue, 04 Sep 2012 13:02:25 +0200 blanchet export "wrap" function
Tue, 04 Sep 2012 12:12:03 +0200 traytel eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
Tue, 04 Sep 2012 12:10:19 +0200 traytel no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
Tue, 04 Sep 2012 00:16:03 +0200 wenzelm enable parallel terminal proofs in interaction;
Mon, 03 Sep 2012 23:03:54 +0200 wenzelm misc tuning;
Mon, 03 Sep 2012 22:51:33 +0200 wenzelm merged
Mon, 03 Sep 2012 18:12:59 +0200 traytel killed internal output
Mon, 03 Sep 2012 17:57:34 +0200 traytel generate coinductive witnesses for codatatypes
Mon, 03 Sep 2012 17:56:39 +0200 traytel generalized signature
Mon, 03 Sep 2012 17:55:42 +0200 traytel added examples for testing of coinductive witnesses
Mon, 03 Sep 2012 22:50:07 +0200 wenzelm continue with more robust dummy session after failed startup;
Mon, 03 Sep 2012 22:31:27 +0200 wenzelm prefer old startup dialog scheme (cf. 514bb82514df);
Mon, 03 Sep 2012 22:22:38 +0200 wenzelm more permissive handling of plugin startup failure;
Mon, 03 Sep 2012 21:30:34 +0200 wenzelm bypass slow check for inlined files, where it is not really required;
Mon, 03 Sep 2012 20:57:51 +0200 wenzelm more direct access to all-important chunks for text painting;
Mon, 03 Sep 2012 15:50:41 +0200 nipkow merged
Mon, 03 Sep 2012 15:41:06 +0200 nipkow added annotations after condition in if and while
Mon, 03 Sep 2012 13:19:52 +0200 wenzelm merge, resolving trivial conflict;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip