haftmann [Sun, 26 May 2013 19:45:54 +0200] rev 52152
examples for interpretation into target
blanchet [Sun, 26 May 2013 14:02:03 +0200] rev 52151
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)
blanchet [Sun, 26 May 2013 12:56:37 +0200] rev 52150
handle lambda-lifted problems in Isar construction code
nipkow [Sun, 26 May 2013 11:56:55 +0200] rev 52149
simpler proof through custom summation function
wenzelm [Sat, 25 May 2013 18:30:38 +0200] rev 52148
merged
wenzelm [Sat, 25 May 2013 17:40:44 +0200] rev 52147
tuned;
wenzelm [Sat, 25 May 2013 17:13:34 +0200] rev 52146
tuned;
wenzelm [Sat, 25 May 2013 17:08:43 +0200] rev 52145
tuned;
wenzelm [Sat, 25 May 2013 16:55:27 +0200] rev 52144
tuned;
wenzelm [Sat, 25 May 2013 15:37:53 +0200] rev 52143
syntax translations always depend on context;
wenzelm [Sat, 25 May 2013 15:00:53 +0200] rev 52142
updated keywords;
haftmann [Sat, 25 May 2013 15:44:29 +0200] rev 52141
weaker precendence of syntax for big intersection and union on sets
haftmann [Sat, 25 May 2013 15:44:08 +0200] rev 52140
tuned structure
noschinl [Sat, 25 May 2013 13:59:08 +0200] rev 52139
add lemma
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52138
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52137
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52136
dedicated module for code symbol data
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52135
symbol data covers class relations also
wenzelm [Fri, 24 May 2013 22:07:01 +0200] rev 52134
merged
wenzelm [Fri, 24 May 2013 17:14:06 +0200] rev 52133
proper internal error, not user error;
wenzelm [Fri, 24 May 2013 17:04:04 +0200] rev 52132
tuned;
wenzelm [Fri, 24 May 2013 17:00:46 +0200] rev 52131
tuned signature;
wenzelm [Fri, 24 May 2013 16:42:57 +0200] rev 52130
tuned;
wenzelm [Fri, 24 May 2013 15:32:02 +0200] rev 52129
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
wenzelm [Fri, 24 May 2013 15:13:25 +0200] rev 52128
tuned signature -- slightly more general operations (cf. term.ML);
wenzelm [Fri, 24 May 2013 14:31:44 +0200] rev 52127
re-use Pattern.unify_types, including its trace_unify_fail option;
wenzelm [Fri, 24 May 2013 14:00:10 +0200] rev 52126
tuned signature;
tuned comments;
blanchet [Fri, 24 May 2013 16:43:37 +0200] rev 52125
improved handling of free variables' types in Isar proofs
blanchet [Fri, 24 May 2013 11:08:25 +0200] rev 52124
pass noninteractive flag -- necessary to run under CASC's "runsolver" program
blanchet [Fri, 24 May 2013 11:08:22 +0200] rev 52123
untabify
noschinl [Thu, 23 May 2013 14:22:49 +0200] rev 52122
more lemmas for sorted_list_of_set
kleing [Thu, 23 May 2013 13:51:21 +1000] rev 52121
prefer object equality
kleing [Thu, 23 May 2013 11:39:40 +1000] rev 52120
slightly clearer formulation
haftmann [Wed, 22 May 2013 22:56:17 +0200] rev 52119
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
haftmann [Wed, 22 May 2013 22:56:17 +0200] rev 52118
mark local theory as brittle also after interpretation inside locales;
more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1;
check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory
wenzelm [Wed, 22 May 2013 19:44:51 +0200] rev 52117
merged
wenzelm [Wed, 22 May 2013 18:10:54 +0200] rev 52116
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm [Wed, 22 May 2013 16:47:48 +0200] rev 52115
tuned signature;
wenzelm [Wed, 22 May 2013 16:42:13 +0200] rev 52114
more informative Build.build_results;
tuned;
wenzelm [Wed, 22 May 2013 16:13:52 +0200] rev 52113
stop protocol handlers as well;
wenzelm [Wed, 22 May 2013 16:01:08 +0200] rev 52112
more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
wenzelm [Wed, 22 May 2013 14:10:45 +0200] rev 52111
explicit management of Session.Protocol_Handlers, with protocol state and functions;
more self-contained ML/Scala module Invoke_Scala;
smolkas [Wed, 22 May 2013 12:39:09 +0200] rev 52110
prevent pretty printer from automatically annotating numerals
smolkas [Wed, 22 May 2013 12:39:07 +0200] rev 52109
tuned
nipkow [Wed, 22 May 2013 08:46:39 +0200] rev 52108
simplified example and proof
nipkow [Wed, 22 May 2013 00:30:36 +0200] rev 52107
tuned
wenzelm [Tue, 21 May 2013 21:05:10 +0200] rev 52106
tuned messages;
wenzelm [Tue, 21 May 2013 18:03:36 +0200] rev 52105
proper options;
tuned;
wenzelm [Tue, 21 May 2013 17:55:28 +0200] rev 52104
proper options;
wenzelm [Tue, 21 May 2013 17:45:53 +0200] rev 52103
more markup;
wenzelm [Tue, 21 May 2013 16:51:16 +0200] rev 52102
tuned;
wenzelm [Tue, 21 May 2013 16:47:18 +0200] rev 52101
less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
wenzelm [Tue, 21 May 2013 13:22:47 +0200] rev 52100
proper context;
wenzelm [Tue, 21 May 2013 12:03:05 +0200] rev 52099
make SML/NJ happy;
blanchet [Tue, 21 May 2013 11:01:14 +0200] rev 52098
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet [Tue, 21 May 2013 09:02:58 +0200] rev 52097
disabled choice in Satallax
blanchet [Tue, 21 May 2013 09:02:58 +0200] rev 52096
use HOL-TPTP image in TPTP tools (for less verbose and faster startup) and filter out some messages
blanchet [Tue, 21 May 2013 09:02:58 +0200] rev 52095
prefer compiled version of LEO-II and Satallax if available
blanchet [Tue, 21 May 2013 09:02:58 +0200] rev 52094
updated remote provers
blanchet [Tue, 21 May 2013 09:02:58 +0200] rev 52093
added compatibility alias