Tue, 28 May 2013 13:22:06 +0200 popescua merged
Tue, 28 May 2013 13:19:51 +0200 popescua merged Well_Order_Extension into Zorn
Tue, 28 May 2013 13:14:31 +0200 wenzelm removed junk (cf. 667961fa6a60);
Tue, 28 May 2013 10:18:43 +0200 blanchet exported ML function
Tue, 28 May 2013 08:52:41 +0200 blanchet redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
Tue, 28 May 2013 08:36:12 +0200 blanchet clean up list of theorems
Tue, 28 May 2013 08:36:11 +0200 blanchet removed needless comment (yes, sum_case_if is needed)
Tue, 28 May 2013 08:29:35 +0200 nipkow tuned
Mon, 27 May 2013 22:32:28 +0200 wenzelm actually test theory Order_Union;
Mon, 27 May 2013 22:30:07 +0200 wenzelm more direct notation;
Mon, 27 May 2013 22:26:08 +0200 wenzelm merged
Mon, 27 May 2013 22:25:32 +0200 wenzelm more literal tokens, e.g. "EX!";
Mon, 27 May 2013 22:00:24 +0200 wenzelm report markup for ast translations;
Mon, 27 May 2013 21:00:30 +0200 wenzelm tuned;
Mon, 27 May 2013 18:39:21 +0200 wenzelm tuned;
Mon, 27 May 2013 18:24:38 +0200 wenzelm discontinued obsolete show_all_types;
Mon, 27 May 2013 20:09:20 +0200 popescua added Ordered_Union
Fri, 24 May 2013 19:09:56 +0200 popescua fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
Fri, 24 May 2013 18:11:57 +0200 popescua well-order extension (by Christian Sternagel)
Fri, 24 May 2013 17:37:06 +0200 popescua modernized Zorn (by Christian Sternagel)
Mon, 27 May 2013 16:53:21 +0200 wenzelm merged
Mon, 27 May 2013 16:52:39 +0200 wenzelm more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
Mon, 27 May 2013 15:57:38 +0200 wenzelm instantiate types as well (see also Thm.first_order_match);
Mon, 27 May 2013 13:55:04 +0200 wenzelm tuned;
Mon, 27 May 2013 13:44:02 +0200 wenzelm updated to ProofGeneral-4.2;
Mon, 27 May 2013 12:40:50 +0200 wenzelm uniform Term_Position.markers (cf. dbadb4d03cbc);
Mon, 27 May 2013 15:14:41 +0200 blanchet get rid of "show_all_types" in Nitpick
Mon, 27 May 2013 15:13:34 +0200 blanchet tuning
Mon, 27 May 2013 15:00:01 +0200 blanchet killed dead argument
Mon, 27 May 2013 14:00:32 +0200 blanchet tuning
Mon, 27 May 2013 13:30:08 +0200 blanchet generalized "mk_co_iter" to handle mutualized (co)iterators
Mon, 27 May 2013 12:21:17 +0200 blanchet tuning
Mon, 27 May 2013 10:13:51 +0200 nipkow tuned
Mon, 27 May 2013 09:15:26 +0200 nipkow tuned
Mon, 27 May 2013 07:44:10 +0200 nipkow merged
Mon, 27 May 2013 07:42:10 +0200 nipkow tuned
Sun, 26 May 2013 22:57:48 +0200 wenzelm merged
Sun, 26 May 2013 22:47:00 +0200 wenzelm position constraint for bound dummy -- more PIDE markup;
Sun, 26 May 2013 21:53:10 +0200 wenzelm position constraint for dummy_pattern -- more PIDE markup;
Sun, 26 May 2013 21:05:03 +0200 wenzelm tuned;
Sun, 26 May 2013 20:42:43 +0200 wenzelm tuned signature;
Sun, 26 May 2013 20:08:53 +0200 wenzelm tuned -- less ML compiler warnings;
Sun, 26 May 2013 20:03:47 +0200 wenzelm more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
Sun, 26 May 2013 19:29:15 +0200 wenzelm more uniform context;
Sun, 26 May 2013 19:27:32 +0200 wenzelm tuned signature;
Sun, 26 May 2013 19:11:52 +0200 wenzelm more conventional pretty printing;
Sun, 26 May 2013 18:37:43 +0200 wenzelm tuned white-space;
Sun, 26 May 2013 19:45:54 +0200 haftmann more specific structure for registration into theory and dependency onto locale
Sun, 26 May 2013 19:45:54 +0200 haftmann examples for interpretation into target
Sun, 26 May 2013 14:02:03 +0200 blanchet disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
Sun, 26 May 2013 12:56:37 +0200 blanchet handle lambda-lifted problems in Isar construction code
Sun, 26 May 2013 11:56:55 +0200 nipkow simpler proof through custom summation function
Sat, 25 May 2013 18:30:38 +0200 wenzelm merged
Sat, 25 May 2013 17:40:44 +0200 wenzelm tuned;
Sat, 25 May 2013 17:13:34 +0200 wenzelm tuned;
Sat, 25 May 2013 17:08:43 +0200 wenzelm tuned;
Sat, 25 May 2013 16:55:27 +0200 wenzelm tuned;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Sat, 25 May 2013 15:00:53 +0200 wenzelm updated keywords;
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip