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
Sat, 25 May 2013 15:44:08 +0200 haftmann tuned structure
Sat, 25 May 2013 13:59:08 +0200 noschinl add lemma
Fri, 24 May 2013 23:57:24 +0200 haftmann bookkeeping and input syntax for exact specification of names of symbols in generated code
Fri, 24 May 2013 23:57:24 +0200 haftmann use generic data for code symbols for unified "code_printing" syntax for custom serialisations
Fri, 24 May 2013 23:57:24 +0200 haftmann dedicated module for code symbol data
Fri, 24 May 2013 23:57:24 +0200 haftmann symbol data covers class relations also
Fri, 24 May 2013 22:07:01 +0200 wenzelm merged
Fri, 24 May 2013 17:14:06 +0200 wenzelm proper internal error, not user error;
Fri, 24 May 2013 17:04:04 +0200 wenzelm tuned;
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Fri, 24 May 2013 16:42:57 +0200 wenzelm tuned;
Fri, 24 May 2013 15:32:02 +0200 wenzelm unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
Fri, 24 May 2013 15:13:25 +0200 wenzelm tuned signature -- slightly more general operations (cf. term.ML);
Fri, 24 May 2013 14:31:44 +0200 wenzelm re-use Pattern.unify_types, including its trace_unify_fail option;
Fri, 24 May 2013 14:00:10 +0200 wenzelm tuned signature;
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs
Fri, 24 May 2013 11:08:25 +0200 blanchet pass noninteractive flag -- necessary to run under CASC's "runsolver" program
Fri, 24 May 2013 11:08:22 +0200 blanchet untabify
Thu, 23 May 2013 14:22:49 +0200 noschinl more lemmas for sorted_list_of_set
Thu, 23 May 2013 13:51:21 +1000 kleing prefer object equality
Thu, 23 May 2013 11:39:40 +1000 kleing slightly clearer formulation
Wed, 22 May 2013 22:56:17 +0200 haftmann interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
Wed, 22 May 2013 22:56:17 +0200 haftmann mark local theory as brittle also after interpretation inside locales;
Wed, 22 May 2013 19:44:51 +0200 wenzelm merged
Wed, 22 May 2013 18:10:54 +0200 wenzelm added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
Wed, 22 May 2013 16:47:48 +0200 wenzelm tuned signature;
Wed, 22 May 2013 16:42:13 +0200 wenzelm more informative Build.build_results;
Wed, 22 May 2013 16:13:52 +0200 wenzelm stop protocol handlers as well;
Wed, 22 May 2013 16:01:08 +0200 wenzelm more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
Wed, 22 May 2013 14:10:45 +0200 wenzelm explicit management of Session.Protocol_Handlers, with protocol state and functions;
Wed, 22 May 2013 12:39:09 +0200 smolkas prevent pretty printer from automatically annotating numerals
Wed, 22 May 2013 12:39:07 +0200 smolkas tuned
Wed, 22 May 2013 08:46:39 +0200 nipkow simplified example and proof
Wed, 22 May 2013 00:30:36 +0200 nipkow tuned
Tue, 21 May 2013 21:05:10 +0200 wenzelm tuned messages;
Tue, 21 May 2013 18:03:36 +0200 wenzelm proper options;
Tue, 21 May 2013 17:55:28 +0200 wenzelm proper options;
Tue, 21 May 2013 17:45:53 +0200 wenzelm more markup;
Tue, 21 May 2013 16:51:16 +0200 wenzelm tuned;
Tue, 21 May 2013 16:47:18 +0200 wenzelm less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
Tue, 21 May 2013 13:22:47 +0200 wenzelm proper context;
Tue, 21 May 2013 12:03:05 +0200 wenzelm make SML/NJ happy;
Tue, 21 May 2013 11:01:14 +0200 blanchet added CASC-related files, to keep a public record of the Isabelle submission at the competition
Tue, 21 May 2013 09:02:58 +0200 blanchet disabled choice in Satallax
Tue, 21 May 2013 09:02:58 +0200 blanchet use HOL-TPTP image in TPTP tools (for less verbose and faster startup) and filter out some messages
Tue, 21 May 2013 09:02:58 +0200 blanchet prefer compiled version of LEO-II and Satallax if available
Tue, 21 May 2013 09:02:58 +0200 blanchet updated remote provers
Tue, 21 May 2013 09:02:58 +0200 blanchet added compatibility alias
Mon, 20 May 2013 20:54:11 +0200 wenzelm merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip