| Mon, 27 May 2013 07:42:10 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 26 May 2013 22:57:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 26 May 2013 22:47:00 +0200 |
wenzelm |
position constraint for bound dummy -- more PIDE markup;
|
changeset |
files
|
| Sun, 26 May 2013 21:53:10 +0200 |
wenzelm |
position constraint for dummy_pattern -- more PIDE markup;
|
changeset |
files
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 26 May 2013 20:42:43 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 26 May 2013 20:08:53 +0200 |
wenzelm |
tuned -- less ML compiler warnings;
|
changeset |
files
|
| 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.);
|
changeset |
files
|
| Sun, 26 May 2013 19:29:15 +0200 |
wenzelm |
more uniform context;
|
changeset |
files
|
| Sun, 26 May 2013 19:27:32 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 26 May 2013 19:11:52 +0200 |
wenzelm |
more conventional pretty printing;
|
changeset |
files
|
| Sun, 26 May 2013 18:37:43 +0200 |
wenzelm |
tuned white-space;
|
changeset |
files
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
more specific structure for registration into theory and dependency onto locale
|
changeset |
files
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
examples for interpretation into target
|
changeset |
files
|
| 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)
|
changeset |
files
|
| Sun, 26 May 2013 12:56:37 +0200 |
blanchet |
handle lambda-lifted problems in Isar construction code
|
changeset |
files
|
| Sun, 26 May 2013 11:56:55 +0200 |
nipkow |
simpler proof through custom summation function
|
changeset |
files
|
| Sat, 25 May 2013 18:30:38 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 25 May 2013 17:40:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 17:13:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 17:08:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 16:55:27 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
changeset |
files
|
| Sat, 25 May 2013 15:00:53 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Sat, 25 May 2013 15:44:29 +0200 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
changeset |
files
|
| Sat, 25 May 2013 15:44:08 +0200 |
haftmann |
tuned structure
|
changeset |
files
|
| Sat, 25 May 2013 13:59:08 +0200 |
noschinl |
add lemma
|
changeset |
files
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
bookkeeping and input syntax for exact specification of names of symbols in generated code
|
changeset |
files
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
|
changeset |
files
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
dedicated module for code symbol data
|
changeset |
files
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
symbol data covers class relations also
|
changeset |
files
|
| Fri, 24 May 2013 22:07:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 24 May 2013 17:14:06 +0200 |
wenzelm |
proper internal error, not user error;
|
changeset |
files
|
| Fri, 24 May 2013 17:04:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 24 May 2013 16:42:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| 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!");
|
changeset |
files
|
| Fri, 24 May 2013 15:13:25 +0200 |
wenzelm |
tuned signature -- slightly more general operations (cf. term.ML);
|
changeset |
files
|
| Fri, 24 May 2013 14:31:44 +0200 |
wenzelm |
re-use Pattern.unify_types, including its trace_unify_fail option;
|
changeset |
files
|
| Fri, 24 May 2013 14:00:10 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
changeset |
files
|
| Fri, 24 May 2013 11:08:25 +0200 |
blanchet |
pass noninteractive flag -- necessary to run under CASC's "runsolver" program
|
changeset |
files
|
| Fri, 24 May 2013 11:08:22 +0200 |
blanchet |
untabify
|
changeset |
files
|
| Thu, 23 May 2013 14:22:49 +0200 |
noschinl |
more lemmas for sorted_list_of_set
|
changeset |
files
|
| Thu, 23 May 2013 13:51:21 +1000 |
kleing |
prefer object equality
|
changeset |
files
|
| Thu, 23 May 2013 11:39:40 +1000 |
kleing |
slightly clearer formulation
|
changeset |
files
|
| 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
|
changeset |
files
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
mark local theory as brittle also after interpretation inside locales;
|
changeset |
files
|
| Wed, 22 May 2013 19:44:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Wed, 22 May 2013 16:47:48 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 22 May 2013 16:42:13 +0200 |
wenzelm |
more informative Build.build_results;
|
changeset |
files
|
| Wed, 22 May 2013 16:13:52 +0200 |
wenzelm |
stop protocol handlers as well;
|
changeset |
files
|
| Wed, 22 May 2013 16:01:08 +0200 |
wenzelm |
more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
|
changeset |
files
|
| Wed, 22 May 2013 14:10:45 +0200 |
wenzelm |
explicit management of Session.Protocol_Handlers, with protocol state and functions;
|
changeset |
files
|
| Wed, 22 May 2013 12:39:09 +0200 |
smolkas |
prevent pretty printer from automatically annotating numerals
|
changeset |
files
|
| Wed, 22 May 2013 12:39:07 +0200 |
smolkas |
tuned
|
changeset |
files
|
| Wed, 22 May 2013 08:46:39 +0200 |
nipkow |
simplified example and proof
|
changeset |
files
|
| Wed, 22 May 2013 00:30:36 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 21 May 2013 21:05:10 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|