wenzelm [Thu, 30 May 2013 17:10:13 +0200] rev 52244
misc tuning;
wenzelm [Thu, 30 May 2013 17:02:09 +0200] rev 52243
prefer existing beta_eta_conversion;
wenzelm [Thu, 30 May 2013 16:53:32 +0200] rev 52242
more standard fold/fold_rev;
wenzelm [Thu, 30 May 2013 16:48:50 +0200] rev 52241
tuned import;
wenzelm [Thu, 30 May 2013 16:31:53 +0200] rev 52240
misc tuning;
wenzelm [Thu, 30 May 2013 16:11:14 +0200] rev 52239
prefer existing beta_eta_conversion;
wenzelm [Thu, 30 May 2013 15:51:55 +0200] rev 52238
more standard names;
wenzelm [Thu, 30 May 2013 15:02:33 +0200] rev 52237
simplified method setup;
wenzelm [Thu, 30 May 2013 14:37:06 +0200] rev 52236
tuned -- prefer terminology of tactic / goal state;
wenzelm [Thu, 30 May 2013 14:17:56 +0200] rev 52235
tuned;
wenzelm [Thu, 30 May 2013 13:59:38 +0200] rev 52234
misc tuning;
wenzelm [Thu, 30 May 2013 13:20:04 +0200] rev 52233
tuned;
wenzelm [Thu, 30 May 2013 13:07:23 +0200] rev 52232
tuned signature;
wenzelm [Thu, 30 May 2013 12:56:25 +0200] rev 52231
stay within regular tactic language -- avoid operating on whole proof state;
wenzelm [Thu, 30 May 2013 12:35:40 +0200] rev 52230
standardized aliases;
Andreas Lochbihler [Thu, 30 May 2013 14:37:35 +0200] rev 52229
space between minus sign and number for large negative number literals causes NumberFormatException at run-time
nipkow [Thu, 30 May 2013 08:27:51 +0200] rev 52228
tuned
kleing [Thu, 30 May 2013 13:59:20 +1000] rev 52227
relational version of HoareT
wenzelm [Wed, 29 May 2013 23:11:21 +0200] rev 52226
obsolete;
wenzelm [Wed, 29 May 2013 18:55:37 +0200] rev 52225
resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
wenzelm [Wed, 29 May 2013 18:52:35 +0200] rev 52224
more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
wenzelm [Wed, 29 May 2013 18:25:11 +0200] rev 52223
tuned signature -- more explicit flags for low-level Thm.bicompose;
wenzelm [Wed, 29 May 2013 16:12:05 +0200] rev 52222
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
wenzelm [Wed, 29 May 2013 12:03:58 +0200] rev 52221
tuned signature;
wenzelm [Wed, 29 May 2013 11:53:31 +0200] rev 52220
backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
wenzelm [Wed, 29 May 2013 11:06:38 +0200] rev 52219
observe type annotations in print translations as well, notably type_constraint_tr';
wenzelm [Wed, 29 May 2013 10:47:42 +0200] rev 52218
make SML/NJ happy;
blanchet [Wed, 29 May 2013 03:10:26 +0200] rev 52217
tuning
blanchet [Wed, 29 May 2013 02:35:49 +0200] rev 52216
more work on general recursors
blanchet [Wed, 29 May 2013 02:35:49 +0200] rev 52215
tuning (use lists rather than pairs of lists throughout)
blanchet [Wed, 29 May 2013 02:35:49 +0200] rev 52214
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet [Wed, 29 May 2013 02:35:49 +0200] rev 52213
tuning
wenzelm [Tue, 28 May 2013 23:11:07 +0200] rev 52212
merged
wenzelm [Tue, 28 May 2013 23:06:32 +0200] rev 52211
explicit support for type annotations within printed syntax trees;
eliminated obsolete show_free_types;
wenzelm [Tue, 28 May 2013 16:29:11 +0200] rev 52210
more explicit Printer.type_emphasis, depending on show_type_emphasis;
tuned signature;
blanchet [Tue, 28 May 2013 23:01:28 +0200] rev 52209
tuning (refactoring)
blanchet [Tue, 28 May 2013 22:20:25 +0200] rev 52208
refactored triplicated functionality
blanchet [Tue, 28 May 2013 21:17:48 +0200] rev 52207
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet [Tue, 28 May 2013 20:00:29 +0200] rev 52206
merge
blanchet [Tue, 28 May 2013 19:59:54 +0200] rev 52205
don't create needless constant
popescua [Tue, 28 May 2013 18:51:29 +0200] rev 52204
merged
popescua [Tue, 28 May 2013 16:56:49 +0200] rev 52203
fixed broken Cardinals and BNF due to Order_Union
blanchet [Tue, 28 May 2013 18:17:40 +0200] rev 52202
no confusing special behavior in debug mode
blanchet [Tue, 28 May 2013 18:12:21 +0200] rev 52201
tuned Nitpick message to be in sync with similar warning from Kodkod
popescua [Tue, 28 May 2013 13:22:06 +0200] rev 52200
merged
popescua [Tue, 28 May 2013 13:19:51 +0200] rev 52199
merged Well_Order_Extension into Zorn
wenzelm [Tue, 28 May 2013 13:14:31 +0200] rev 52198
removed junk (cf. 667961fa6a60);
blanchet [Tue, 28 May 2013 10:18:43 +0200] rev 52197
exported ML function
blanchet [Tue, 28 May 2013 08:52:41 +0200] rev 52196
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet [Tue, 28 May 2013 08:36:12 +0200] rev 52195
clean up list of theorems
blanchet [Tue, 28 May 2013 08:36:11 +0200] rev 52194
removed needless comment (yes, sum_case_if is needed)
nipkow [Tue, 28 May 2013 08:29:35 +0200] rev 52193
tuned
wenzelm [Mon, 27 May 2013 22:32:28 +0200] rev 52192
actually test theory Order_Union;
wenzelm [Mon, 27 May 2013 22:30:07 +0200] rev 52191
more direct notation;
wenzelm [Mon, 27 May 2013 22:26:08 +0200] rev 52190
merged
wenzelm [Mon, 27 May 2013 22:25:32 +0200] rev 52189
more literal tokens, e.g. "EX!";
wenzelm [Mon, 27 May 2013 22:00:24 +0200] rev 52188
report markup for ast translations;
wenzelm [Mon, 27 May 2013 21:00:30 +0200] rev 52187
tuned;
wenzelm [Mon, 27 May 2013 18:39:21 +0200] rev 52186
tuned;
wenzelm [Mon, 27 May 2013 18:24:38 +0200] rev 52185
discontinued obsolete show_all_types;
popescua [Mon, 27 May 2013 20:09:20 +0200] rev 52184
added Ordered_Union
popescua [Fri, 24 May 2013 19:09:56 +0200] rev 52183
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua [Fri, 24 May 2013 18:11:57 +0200] rev 52182
well-order extension (by Christian Sternagel)
popescua [Fri, 24 May 2013 17:37:06 +0200] rev 52181
modernized Zorn (by Christian Sternagel)
wenzelm [Mon, 27 May 2013 16:53:21 +0200] rev 52180
merged
wenzelm [Mon, 27 May 2013 16:52:39 +0200] rev 52179
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);
wenzelm [Mon, 27 May 2013 15:57:38 +0200] rev 52178
instantiate types as well (see also Thm.first_order_match);
wenzelm [Mon, 27 May 2013 13:55:04 +0200] rev 52177
tuned;
wenzelm [Mon, 27 May 2013 13:44:02 +0200] rev 52176
updated to ProofGeneral-4.2;
wenzelm [Mon, 27 May 2013 12:40:50 +0200] rev 52175
uniform Term_Position.markers (cf. dbadb4d03cbc);
blanchet [Mon, 27 May 2013 15:14:41 +0200] rev 52174
get rid of "show_all_types" in Nitpick
blanchet [Mon, 27 May 2013 15:13:34 +0200] rev 52173
tuning
blanchet [Mon, 27 May 2013 15:00:01 +0200] rev 52172
killed dead argument
blanchet [Mon, 27 May 2013 14:00:32 +0200] rev 52171
tuning
blanchet [Mon, 27 May 2013 13:30:08 +0200] rev 52170
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet [Mon, 27 May 2013 12:21:17 +0200] rev 52169
tuning
nipkow [Mon, 27 May 2013 10:13:51 +0200] rev 52168
tuned
nipkow [Mon, 27 May 2013 09:15:26 +0200] rev 52167
tuned
nipkow [Mon, 27 May 2013 07:44:10 +0200] rev 52166
merged
nipkow [Mon, 27 May 2013 07:42:10 +0200] rev 52165
tuned
wenzelm [Sun, 26 May 2013 22:57:48 +0200] rev 52164
merged
wenzelm [Sun, 26 May 2013 22:47:00 +0200] rev 52163
position constraint for bound dummy -- more PIDE markup;
wenzelm [Sun, 26 May 2013 21:53:10 +0200] rev 52162
position constraint for dummy_pattern -- more PIDE markup;
wenzelm [Sun, 26 May 2013 21:05:03 +0200] rev 52161
tuned;
wenzelm [Sun, 26 May 2013 20:42:43 +0200] rev 52160
tuned signature;
wenzelm [Sun, 26 May 2013 20:08:53 +0200] rev 52159
tuned -- less ML compiler warnings;
wenzelm [Sun, 26 May 2013 20:03:47 +0200] rev 52158
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm [Sun, 26 May 2013 19:29:15 +0200] rev 52157
more uniform context;
wenzelm [Sun, 26 May 2013 19:27:32 +0200] rev 52156
tuned signature;
wenzelm [Sun, 26 May 2013 19:11:52 +0200] rev 52155
more conventional pretty printing;
more markup;
wenzelm [Sun, 26 May 2013 18:37:43 +0200] rev 52154
tuned white-space;
haftmann [Sun, 26 May 2013 19:45:54 +0200] rev 52153
more specific structure for registration into theory and dependency onto locale
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
wenzelm [Mon, 20 May 2013 20:54:11 +0200] rev 52092
merged
wenzelm [Mon, 20 May 2013 20:49:10 +0200] rev 52091
more rigorous check of simplifier context;
tuned;
wenzelm [Mon, 20 May 2013 20:47:33 +0200] rev 52090
proper context;
wenzelm [Mon, 20 May 2013 18:38:28 +0200] rev 52089
proper context;
wenzelm [Mon, 20 May 2013 18:37:35 +0200] rev 52088
proper run-time context;
wenzelm [Mon, 20 May 2013 17:14:39 +0200] rev 52087
more precise treatment of theory vs. Proof.context;
wenzelm [Mon, 20 May 2013 17:11:17 +0200] rev 52086
proper run-time context;
wenzelm [Mon, 20 May 2013 17:10:33 +0200] rev 52085
tuned;
wenzelm [Mon, 20 May 2013 16:17:56 +0200] rev 52084
more explicit Session.update_options as source of Global_Options event;
wenzelm [Mon, 20 May 2013 15:42:14 +0200] rev 52083
even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);
wenzelm [Mon, 20 May 2013 14:04:21 +0200] rev 52082
tuned;
wenzelm [Mon, 20 May 2013 13:54:24 +0200] rev 52081
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm [Mon, 20 May 2013 13:38:48 +0200] rev 52080
reset options last -- other parts of the system may still need them;
wenzelm [Mon, 20 May 2013 13:29:45 +0200] rev 52079
tuned signature;
blanchet [Mon, 20 May 2013 16:12:33 +0200] rev 52078
updated Sledgehammer docs
blanchet [Mon, 20 May 2013 13:07:31 +0200] rev 52077
parse agsyHOL proofs (as unsat cores)
blanchet [Mon, 20 May 2013 12:35:29 +0200] rev 52076
freeze types in Sledgehammer goal, not just terms
blanchet [Mon, 20 May 2013 11:49:56 +0200] rev 52075
generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet [Mon, 20 May 2013 11:35:55 +0200] rev 52074
tuned code
blanchet [Mon, 20 May 2013 11:27:13 +0200] rev 52073
started adding agsyHOL as an experimental prover
nipkow [Mon, 20 May 2013 03:41:58 +0200] rev 52072
defined lvars and rvars of commands separately.
blanchet [Sun, 19 May 2013 20:41:19 +0200] rev 52071
made "completish" mode a bit more complete
haftmann [Sun, 19 May 2013 20:15:00 +0200] rev 52070
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann [Sun, 19 May 2013 20:15:00 +0200] rev 52069
tuned and clarified
haftmann [Sun, 19 May 2013 20:15:00 +0200] rev 52068
tuned, including signature
wenzelm [Sat, 18 May 2013 13:04:10 +0200] rev 52067
discontinued odd workaround for scala-2.10.0-RC1;
wenzelm [Sat, 18 May 2013 13:00:05 +0200] rev 52066
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm [Sat, 18 May 2013 12:41:31 +0200] rev 52065
explicit notion of public options, which are shown in the editor options dialog;
avoid hard-wired stuff;
wenzelm [Fri, 17 May 2013 23:31:02 +0200] rev 52064
back to more paranoid interrupt test after request is cancelled -- avoid race condition;
wenzelm [Fri, 17 May 2013 21:15:33 +0200] rev 52063
timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
wenzelm [Fri, 17 May 2013 21:06:01 +0200] rev 52062
added isabelle tty option -o;
wenzelm [Fri, 17 May 2013 21:02:08 +0200] rev 52061
oops;
wenzelm [Fri, 17 May 2013 20:53:28 +0200] rev 52060
renamed 'print_configs' to 'print_options';
wenzelm [Fri, 17 May 2013 20:41:45 +0200] rev 52059
proper option quick_and_dirty;
wenzelm [Fri, 17 May 2013 20:30:04 +0200] rev 52058
retain quick_and_dirty as-is -- no censorship;
wenzelm [Fri, 17 May 2013 19:11:03 +0200] rev 52057
more system-atic options;
wenzelm [Fri, 17 May 2013 19:04:52 +0200] rev 52056
added isabelle-process option -o;
wenzelm [Fri, 17 May 2013 18:50:55 +0200] rev 52055
more precise "eval", cf. isabelle build;
wenzelm [Fri, 17 May 2013 18:39:49 +0200] rev 52054
discontinued obsolete isabelle-process options -f and -u;
wenzelm [Fri, 17 May 2013 18:23:39 +0200] rev 52053
NEWS;
wenzelm [Fri, 17 May 2013 18:19:42 +0200] rev 52052
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm [Fri, 17 May 2013 17:45:51 +0200] rev 52051
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm [Fri, 17 May 2013 17:11:06 +0200] rev 52050
event timer as separate service thread;
wenzelm [Fri, 17 May 2013 13:46:18 +0200] rev 52049
tuned signature;
wenzelm [Fri, 17 May 2013 11:35:52 +0200] rev 52048
tuned signature -- emphasize thread creation here;
wenzelm [Fri, 17 May 2013 11:05:59 +0200] rev 52047
repair after bc01725d7918;
nipkow [Fri, 17 May 2013 08:19:52 +0200] rev 52046
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow [Fri, 17 May 2013 02:57:00 +0200] rev 52045
tuned
wenzelm [Thu, 16 May 2013 22:02:01 +0200] rev 52044
merged
wenzelm [Thu, 16 May 2013 21:48:01 +0200] rev 52043
more system options as context-sensitive config options;
wenzelm [Thu, 16 May 2013 21:09:58 +0200] rev 52042
Thy_Output.modes as proper option;
wenzelm [Thu, 16 May 2013 20:50:01 +0200] rev 52041
some system options as context-sensitive config options;
wenzelm [Thu, 16 May 2013 20:33:01 +0200] rev 52040
system options as context-sensitive configuration options within the attribute name space;
wenzelm [Thu, 16 May 2013 19:41:41 +0200] rev 52039
tuned signature;
blanchet [Thu, 16 May 2013 21:55:12 +0200] rev 52038
properly handle SPASS constructors w.r.t. partially applied functions
wenzelm [Thu, 16 May 2013 17:39:38 +0200] rev 52037
tuned signature -- depend on context by default;
kuncar [Thu, 16 May 2013 15:21:12 +0200] rev 52036
reflexivity rules for the function type and equality
blanchet [Thu, 16 May 2013 15:03:28 +0200] rev 52035
tuned comments
blanchet [Thu, 16 May 2013 14:58:30 +0200] rev 52034
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet [Thu, 16 May 2013 14:27:43 +0200] rev 52033
tuning
blanchet [Thu, 16 May 2013 14:15:22 +0200] rev 52032
more work on SPASS datatypes
blanchet [Thu, 16 May 2013 13:34:13 +0200] rev 52031
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet [Thu, 16 May 2013 13:19:27 +0200] rev 52030
compile
blanchet [Thu, 16 May 2013 13:05:52 +0200] rev 52029
don't recognize overloaded constants as constructors for the purpose of removing type arguments
blanchet [Thu, 16 May 2013 13:05:52 +0200] rev 52028
tuning
blanchet [Thu, 16 May 2013 13:05:52 +0200] rev 52027
reintroduced syntax for "nonexhaustive" datatypes
blanchet [Thu, 16 May 2013 13:05:52 +0200] rev 52026
tuning
blanchet [Thu, 16 May 2013 13:05:52 +0200] rev 52025
more work on SPASS datatypes
Andreas Lochbihler [Thu, 16 May 2013 11:35:07 +0200] rev 52024
merged
Andreas Lochbihler [Thu, 16 May 2013 10:08:28 +0200] rev 52023
setup for set membership as a predicate for code_pred
nipkow [Thu, 16 May 2013 11:27:34 +0200] rev 52022
tuned
kleing [Thu, 16 May 2013 13:49:18 +1000] rev 52021
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
nipkow [Thu, 16 May 2013 02:13:42 +0200] rev 52020
merged
nipkow [Thu, 16 May 2013 02:13:23 +0200] rev 52019
finally: acom with pointwise access and update of annotations
wenzelm [Wed, 15 May 2013 23:00:17 +0200] rev 52018
merged;
wenzelm [Wed, 15 May 2013 22:30:24 +0200] rev 52017
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm [Wed, 15 May 2013 22:02:51 +0200] rev 52016
simplified ProofGeneral.preference operation -- no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);
wenzelm [Wed, 15 May 2013 21:55:09 +0200] rev 52015
back to hidden welcome -- revert change 9ebf2da69b29, which appears to disturb startup protocol of PG 4.1;
wenzelm [Wed, 15 May 2013 21:46:07 +0200] rev 52014
more standard Isabelle/ML structures for global preferences;
allow to add categories later on;
allow to redefine preferences as usual for global tables, e.g. after reloading ML modules;
wenzelm [Wed, 15 May 2013 21:02:13 +0200] rev 52013
more basic print mode "ProofGeneral" (again);
wenzelm [Wed, 15 May 2013 20:53:42 +0200] rev 52012
uniform welcome -- actually visible on startup via Output.urgent_message;
tuned;
wenzelm [Wed, 15 May 2013 20:45:27 +0200] rev 52011
more elementary ProofGeneral.thm_deps;
wenzelm [Wed, 15 May 2013 20:39:25 +0200] rev 52010
tuned;
wenzelm [Wed, 15 May 2013 20:34:42 +0200] rev 52009
moved files;
wenzelm [Wed, 15 May 2013 20:28:43 +0200] rev 52008
clarified default for Proofterm.proofs, according to etc/options and innermost setmp;
wenzelm [Wed, 15 May 2013 20:22:46 +0200] rev 52007
maintain ProofGeneral preferences within ProofGeneral module;
initialize Isabelle/Pure preferences within normal user space (with antiquotations);
tuned;
wenzelm [Wed, 15 May 2013 17:39:41 +0200] rev 52006
just one ProofGeneral module;
blanchet [Wed, 15 May 2013 18:44:19 +0200] rev 52005
tuning
blanchet [Wed, 15 May 2013 18:39:20 +0200] rev 52004
more work on SPASS datatypes
blanchet [Wed, 15 May 2013 18:09:20 +0200] rev 52003
tuning
blanchet [Wed, 15 May 2013 18:06:40 +0200] rev 52002
no need to reinvent the wheel ("fold_map")
blanchet [Wed, 15 May 2013 18:05:46 +0200] rev 52001
more work on implementing datatype output for new SPASS
blanchet [Wed, 15 May 2013 17:49:39 +0200] rev 52000
tuned code
blanchet [Wed, 15 May 2013 17:49:18 +0200] rev 51999
compile
blanchet [Wed, 15 May 2013 17:43:42 +0200] rev 51998
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet [Wed, 15 May 2013 17:27:24 +0200] rev 51997
added datatype declaration syntax for next-gen SPASS
kuncar [Wed, 15 May 2013 12:13:38 +0200] rev 51996
abstract equalities only in a correspondence relation in a transfer domain rule
kuncar [Wed, 15 May 2013 12:10:44 +0200] rev 51995
superfluous transfer rule
kuncar [Wed, 15 May 2013 12:10:39 +0200] rev 51994
stronger reflexivity prover
wenzelm [Tue, 14 May 2013 21:56:19 +0200] rev 51993
simplified modules and exceptions;
wenzelm [Tue, 14 May 2013 21:40:25 +0200] rev 51992
more elementary pgiptype;
wenzelm [Tue, 14 May 2013 21:02:49 +0200] rev 51991
prefer Markup.parse/print operations -- slight change of exception behaviour;
removed obsolete PGIP material;
wenzelm [Tue, 14 May 2013 20:46:09 +0200] rev 51990
more uniform Markup.print_real;
wenzelm [Tue, 14 May 2013 20:32:10 +0200] rev 51989
removed dead code;
wenzelm [Tue, 14 May 2013 19:48:31 +0200] rev 51988
more uniform Markup.parse_real;
wenzelm [Tue, 14 May 2013 19:30:21 +0200] rev 51987
tuned signature;
wenzelm [Tue, 14 May 2013 16:54:47 +0200] rev 51986
more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError;
wenzelm [Tue, 14 May 2013 16:45:09 +0200] rev 51985
tuned;
wenzelm [Tue, 14 May 2013 16:04:26 +0200] rev 51984
misc tuning and simplification;
wenzelm [Tue, 14 May 2013 15:40:18 +0200] rev 51983
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm [Tue, 14 May 2013 14:17:56 +0200] rev 51982
more scalable File.write via separate chunks;
tuned signature of File.write_xz: prefer defaults over overloading;
wenzelm [Tue, 14 May 2013 13:46:33 +0200] rev 51981
more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm [Tue, 14 May 2013 12:46:26 +0200] rev 51980
support for more informative crashes;
wenzelm [Tue, 14 May 2013 12:31:11 +0200] rev 51979
more antiquotations;
wenzelm [Tue, 14 May 2013 12:22:18 +0200] rev 51978
tuned messages;
wenzelm [Tue, 14 May 2013 12:21:35 +0200] rev 51977
more generous java resources via ISABELLE_BUILD_JAVA_OPTIONS;
blanchet [Tue, 14 May 2013 09:49:03 +0200] rev 51976
generate valid direct Isar proof also if the facts are contradictory
nipkow [Tue, 14 May 2013 07:09:09 +0200] rev 51975
tuned names
nipkow [Tue, 14 May 2013 06:54:31 +0200] rev 51974
tuned names
wenzelm [Mon, 13 May 2013 22:49:00 +0200] rev 51973
removed obsolete PGIP material;
wenzelm [Mon, 13 May 2013 22:26:59 +0200] rev 51972
more direct output of remaining PGIP rudiments;
tuned signature;
wenzelm [Mon, 13 May 2013 22:12:24 +0200] rev 51971
simplified preferences, removed obsolete operations;
wenzelm [Mon, 13 May 2013 22:00:19 +0200] rev 51970
tuned signature;
wenzelm [Mon, 13 May 2013 21:42:27 +0200] rev 51969
more direct output of remaining PGIP rudiments;
wenzelm [Mon, 13 May 2013 21:07:01 +0200] rev 51968
obsolete;
wenzelm [Mon, 13 May 2013 21:03:30 +0200] rev 51967
removed obsolete PGIP material;
wenzelm [Mon, 13 May 2013 20:35:04 +0200] rev 51966
recovered informative progress from 016cb7d8f297;
wenzelm [Mon, 13 May 2013 20:30:49 +0200] rev 51965
removed obsolete PGIP material;
wenzelm [Mon, 13 May 2013 20:26:34 +0200] rev 51964
clean startup of RAW session;
wenzelm [Mon, 13 May 2013 20:15:06 +0200] rev 51963
dummy PGIP id, which appears to be sufficient for PG/Emacs;
removed obsolete init operations;
wenzelm [Mon, 13 May 2013 19:52:16 +0200] rev 51962
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm [Mon, 13 May 2013 16:40:59 +0200] rev 51961
merged
wenzelm [Mon, 13 May 2013 13:23:13 +0200] rev 51960
option "goals_limit", with more uniform description;
wenzelm [Mon, 13 May 2013 13:01:10 +0200] rev 51959
clarified message when subgoals have been stripped -- unconditional;
wenzelm [Mon, 13 May 2013 12:40:17 +0200] rev 51958
retain goal display options when printing error messages, to avoid breakdown for huge goals;
kuncar [Mon, 13 May 2013 15:22:19 +0200] rev 51957
typo
kuncar [Mon, 13 May 2013 13:59:04 +0200] rev 51956
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar [Mon, 13 May 2013 12:13:24 +0200] rev 51955
try to detect assumptions of transfer rules that are in a shape of a transfer rule
kuncar [Mon, 13 May 2013 12:13:24 +0200] rev 51954
publish a private function
nipkow [Mon, 13 May 2013 06:50:37 +0200] rev 51953
tuned names
wenzelm [Sun, 12 May 2013 20:58:01 +0200] rev 51952
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;
wenzelm [Sun, 12 May 2013 20:46:17 +0200] rev 51951
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm [Sun, 12 May 2013 20:30:34 +0200] rev 51950
prefer standard Isabelle/ML operations;
wenzelm [Sun, 12 May 2013 20:25:45 +0200] rev 51949
some system options as context-sensitive config options;
wenzelm [Sun, 12 May 2013 19:56:30 +0200] rev 51948
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
wenzelm [Sun, 12 May 2013 18:22:44 +0200] rev 51947
support for system options as context-sensitive config options;
wenzelm [Sun, 12 May 2013 18:20:16 +0200] rev 51946
tuned signature;
wenzelm [Sun, 12 May 2013 17:56:53 +0200] rev 51945
tuned comments;
wenzelm [Sun, 12 May 2013 17:51:34 +0200] rev 51944
support for options as preferences;
wenzelm [Sun, 12 May 2013 17:42:36 +0200] rev 51943
more operations in accordance to Scala version;
wenzelm [Sun, 12 May 2013 15:08:11 +0200] rev 51942
more systematic access to options default;
wenzelm [Sun, 12 May 2013 15:05:15 +0200] rev 51941
full default options for Isabelle_Process and Build;
wenzelm [Sun, 12 May 2013 14:25:16 +0200] rev 51940
decentralized historic settings;
wenzelm [Sun, 12 May 2013 13:56:21 +0200] rev 51939
removed obsolete test_markup;
tuned;
wenzelm [Sun, 12 May 2013 13:46:41 +0200] rev 51938
Proof General interaction always uses Isar loop;
pass Isabelle/Scala options to Proof General process as well;
wenzelm [Sun, 12 May 2013 13:08:23 +0200] rev 51937
proper context;
wenzelm [Sat, 11 May 2013 22:20:59 +0200] rev 51936
merged
wenzelm [Sat, 11 May 2013 22:17:18 +0200] rev 51935
more direct PGIP/Emacs processing and output;
wenzelm [Sat, 11 May 2013 21:34:53 +0200] rev 51934
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm [Sat, 11 May 2013 20:10:24 +0200] rev 51933
removed redundant modules;
wenzelm [Sat, 11 May 2013 18:45:38 +0200] rev 51932
removed some obsolete PGIP/PGEclipse material;
wenzelm [Sat, 11 May 2013 18:16:17 +0200] rev 51931
never open structure Unsynchronized (cf. "implementation" manual);
wenzelm [Sat, 11 May 2013 16:57:18 +0200] rev 51930
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm [Sat, 11 May 2013 16:13:08 +0200] rev 51929
avoid PolyML.makestring, even in dead code;
blanchet [Sat, 11 May 2013 16:00:24 +0200] rev 51928
fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"
kuncar [Fri, 10 May 2013 19:41:23 +0200] rev 51927
don't apply an unnecessary morphism
nipkow [Fri, 10 May 2013 06:34:29 +0200] rev 51926
tuned
traytel [Thu, 09 May 2013 20:44:37 +0200] rev 51925
relator coinduction for codatatypes
nipkow [Thu, 09 May 2013 03:58:28 +0200] rev 51924
standard ivl notation [l,h]
nipkow [Thu, 09 May 2013 02:42:51 +0200] rev 51923
merged
nipkow [Wed, 08 May 2013 12:06:04 +0200] rev 51922
tuned
blanchet [Wed, 08 May 2013 19:16:43 +0200] rev 51921
avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time
blanchet [Wed, 08 May 2013 16:38:02 +0200] rev 51920
proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS
blanchet [Wed, 08 May 2013 15:47:19 +0200] rev 51919
use right default for "uncurried_aliases" with polymorphic SPASS
traytel [Wed, 08 May 2013 13:33:04 +0200] rev 51918
relator induction for datatypes
traytel [Wed, 08 May 2013 11:57:42 +0200] rev 51917
store proper theorems even for fixed points that have no passive live variables
traytel [Wed, 08 May 2013 09:45:30 +0200] rev 51916
stronger monotonicity property for relators
traytel [Wed, 08 May 2013 09:39:30 +0200] rev 51915
make tactic actually work for op = as relator
nipkow [Wed, 08 May 2013 06:14:11 +0200] rev 51914
tuned
nipkow [Wed, 08 May 2013 04:16:44 +0200] rev 51913
hide Fin on output
blanchet [Tue, 07 May 2013 21:37:40 +0200] rev 51912
removed dead argument
blanchet [Tue, 07 May 2013 21:09:47 +0200] rev 51911
more robust iterator construction (needed for mutualized FPs)
blanchet [Tue, 07 May 2013 21:09:46 +0200] rev 51910
tuning
traytel [Tue, 07 May 2013 18:40:23 +0200] rev 51909
removed dead internal constants/theorems
blanchet [Tue, 07 May 2013 17:35:29 +0200] rev 51908
removed tracing
blanchet [Tue, 07 May 2013 17:29:23 +0200] rev 51907
export one more function
blanchet [Tue, 07 May 2013 17:07:37 +0200] rev 51906
added field to record
blanchet [Tue, 07 May 2013 16:43:17 +0200] rev 51905
tuning
blanchet [Tue, 07 May 2013 16:18:42 +0200] rev 51904
removed dead code
blanchet [Tue, 07 May 2013 16:15:21 +0200] rev 51903
move function to library
blanchet [Tue, 07 May 2013 15:40:00 +0200] rev 51902
tuning
blanchet [Tue, 07 May 2013 15:32:12 +0200] rev 51901
more
blanchet [Tue, 07 May 2013 15:31:58 +0200] rev 51900
tuning
blanchet [Tue, 07 May 2013 15:11:24 +0200] rev 51899
code tuning
blanchet [Tue, 07 May 2013 15:03:15 +0200] rev 51898
merge
blanchet [Tue, 07 May 2013 15:03:01 +0200] rev 51897
refactoring
blanchet [Tue, 07 May 2013 14:27:39 +0200] rev 51896
export one more function + tuning
traytel [Tue, 07 May 2013 15:20:46 +0200] rev 51895
do not unfold the definition of the relator as it is not defined in terms of srel anymore
traytel [Tue, 07 May 2013 14:47:22 +0200] rev 51894
tuned
traytel [Tue, 07 May 2013 14:22:54 +0200] rev 51893
got rid of the set based relator---use (binary) predicate based relator instead
blanchet [Tue, 07 May 2013 11:27:29 +0200] rev 51892
tuned names + extended ML signature
nipkow [Tue, 07 May 2013 10:35:40 +0200] rev 51891
merged
nipkow [Tue, 07 May 2013 10:34:55 +0200] rev 51890
tuned name: filter -> constrain (longer but more intuitive)
blanchet [Tue, 07 May 2013 10:29:30 +0200] rev 51889
tuning
blanchet [Tue, 07 May 2013 10:18:59 +0200] rev 51888
imported patch refactor_coiter_constr
nipkow [Tue, 07 May 2013 03:24:23 +0200] rev 51887
tuned
blanchet [Mon, 06 May 2013 22:49:26 +0200] rev 51886
started factoring out coiter construction
blanchet [Mon, 06 May 2013 21:29:16 +0200] rev 51885
rationalize ML signature
blanchet [Mon, 06 May 2013 21:20:54 +0200] rev 51884
factor out construction of iterator
blanchet [Mon, 06 May 2013 18:17:45 +0200] rev 51883
tuning
nipkow [Mon, 06 May 2013 15:10:21 +0200] rev 51882
improved defns and proofs
smolkas [Mon, 06 May 2013 11:17:33 +0200] rev 51881
undo 46d911ab9170 since it causes problems
smolkas [Mon, 06 May 2013 11:05:32 +0200] rev 51880
allow '-'s in tptp ids to avoid problems with remote_vampire
smolkas [Mon, 06 May 2013 11:03:08 +0200] rev 51879
added preplay tracing
smolkas [Mon, 06 May 2013 11:03:08 +0200] rev 51878
handle dummy atp terms
smolkas [Mon, 06 May 2013 11:03:08 +0200] rev 51877
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
smolkas [Mon, 06 May 2013 11:03:08 +0200] rev 51876
added informative error messages
nipkow [Mon, 06 May 2013 02:48:18 +0200] rev 51875
tail recursive version of map, for code generation, optionally
nipkow [Mon, 06 May 2013 00:25:04 +0200] rev 51874
simplified proofs
blanchet [Fri, 03 May 2013 10:27:24 +0200] rev 51873
tuning
blanchet [Fri, 03 May 2013 10:26:34 +0200] rev 51872
pass certain readability-enhancing Vampire options only when an Isar proof is needed
nipkow [Fri, 03 May 2013 05:25:14 +0200] rev 51871
added lemma
nipkow [Fri, 03 May 2013 02:52:25 +0200] rev 51870
added lemma
blanchet [Thu, 02 May 2013 21:04:50 +0200] rev 51869
renamings
blanchet [Thu, 02 May 2013 18:48:39 +0200] rev 51868
code tuning
blanchet [Thu, 02 May 2013 18:34:36 +0200] rev 51867
signature tuning
blanchet [Thu, 02 May 2013 18:25:44 +0200] rev 51866
removed dead code
blanchet [Thu, 02 May 2013 18:16:28 +0200] rev 51865
tuned signature
blanchet [Thu, 02 May 2013 16:33:04 +0200] rev 51864
store (co)induction rules in data structure
blanchet [Thu, 02 May 2013 16:14:14 +0200] rev 51863
tuning names
blanchet [Thu, 02 May 2013 15:28:11 +0200] rev 51862
got rid of needless library function (find_minimum)
blanchet [Thu, 02 May 2013 15:08:59 +0200] rev 51861
one more lib function
blanchet [Thu, 02 May 2013 14:04:56 +0200] rev 51860
export one more function
blanchet [Thu, 02 May 2013 12:35:02 +0200] rev 51859
rationalized data structure
blanchet [Thu, 02 May 2013 11:58:18 +0200] rev 51858
added and moved library functions (used in primrec code)
blanchet [Thu, 02 May 2013 11:19:05 +0200] rev 51857
tuned names -- co_ and un_ with underscore are to be understood as (co) and (un)
blanchet [Thu, 02 May 2013 10:16:40 +0200] rev 51856
tuning
blanchet [Thu, 02 May 2013 10:11:14 +0200] rev 51855
more code rationalization
blanchet [Thu, 02 May 2013 10:05:30 +0200] rev 51854
more code rationalization
blanchet [Thu, 02 May 2013 09:50:58 +0200] rev 51853
more code rationalization
blanchet [Thu, 02 May 2013 09:41:29 +0200] rev 51852
refactoring
nipkow [Thu, 02 May 2013 03:13:47 +0200] rev 51851
tuned
blanchet [Wed, 01 May 2013 19:33:49 +0200] rev 51850
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
nipkow [Wed, 01 May 2013 06:00:55 +0200] rev 51849
tuned
nipkow [Wed, 01 May 2013 03:56:57 +0200] rev 51848
tuned
blanchet [Tue, 30 Apr 2013 21:30:36 +0200] rev 51847
tuning
blanchet [Tue, 30 Apr 2013 18:43:48 +0200] rev 51846
export more functions (useful for primrec_new)
blanchet [Tue, 30 Apr 2013 17:22:51 +0200] rev 51845
further enrich data structure
blanchet [Tue, 30 Apr 2013 16:50:09 +0200] rev 51844
more
blanchet [Tue, 30 Apr 2013 16:42:23 +0200] rev 51843
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet [Tue, 30 Apr 2013 16:29:31 +0200] rev 51842
added fields to database
blanchet [Tue, 30 Apr 2013 16:18:21 +0200] rev 51841
tuned data structure
blanchet [Tue, 30 Apr 2013 16:04:50 +0200] rev 51840
renamed records
blanchet [Tue, 30 Apr 2013 15:58:32 +0200] rev 51839
added constructors to data structure
blanchet [Tue, 30 Apr 2013 13:45:43 +0200] rev 51838
added pre-BNFs to database
blanchet [Tue, 30 Apr 2013 13:38:41 +0200] rev 51837
lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
blanchet [Tue, 30 Apr 2013 13:34:31 +0200] rev 51836
renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
blanchet [Tue, 30 Apr 2013 13:23:52 +0200] rev 51835
Added maps, sets, rels to "simps" thm collection
nipkow [Tue, 30 Apr 2013 12:26:41 +0200] rev 51834
tuned
blanchet [Tue, 30 Apr 2013 12:18:40 +0200] rev 51833
comment tuning
blanchet [Tue, 30 Apr 2013 12:13:28 +0200] rev 51832
tuning
blanchet [Tue, 30 Apr 2013 11:59:20 +0200] rev 51831
tuning
blanchet [Tue, 30 Apr 2013 11:28:43 +0200] rev 51830
tuning
blanchet [Tue, 30 Apr 2013 10:58:25 +0200] rev 51829
signature tuning
blanchet [Tue, 30 Apr 2013 10:07:41 +0200] rev 51828
whitespace tuning
blanchet [Tue, 30 Apr 2013 09:53:56 +0200] rev 51827
tuned signature
nipkow [Tue, 30 Apr 2013 03:18:07 +0200] rev 51826
canonical names of classes
blanchet [Mon, 29 Apr 2013 18:52:35 +0200] rev 51825
merged
blanchet [Mon, 29 Apr 2013 18:52:18 +0200] rev 51824
register all (co)datatypes in local data
blanchet [Mon, 29 Apr 2013 17:37:00 +0200] rev 51823
create data structure for storing (co)datatype information
wenzelm [Mon, 29 Apr 2013 17:17:20 +0200] rev 51822
avoid empty isabelletags.sty for the sake of arXiv;
wenzelm [Mon, 29 Apr 2013 17:08:57 +0200] rev 51821
merged
wenzelm [Mon, 29 Apr 2013 17:01:13 +0200] rev 51820
cygwin_root as optional argument;
tuned;
blanchet [Mon, 29 Apr 2013 16:50:01 +0200] rev 51819
use record instead of big tuple
wenzelm [Mon, 29 Apr 2013 15:47:42 +0200] rev 51818
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
blanchet [Mon, 29 Apr 2013 14:07:03 +0200] rev 51817
merge
blanchet [Mon, 29 Apr 2013 14:06:37 +0200] rev 51816
use base names, not full names
blanchet [Mon, 29 Apr 2013 13:52:14 +0200] rev 51815
tune signatures
blanchet [Mon, 29 Apr 2013 13:47:46 +0200] rev 51814
tuning
blanchet [Mon, 29 Apr 2013 13:42:54 +0200] rev 51813
tuning
blanchet [Mon, 29 Apr 2013 13:41:34 +0200] rev 51812
removed unreferenced thm
blanchet [Mon, 29 Apr 2013 13:40:26 +0200] rev 51811
tuned function signatures
blanchet [Mon, 29 Apr 2013 11:46:03 +0200] rev 51810
factored out derivation of coinduction, unfold, corec
blanchet [Mon, 29 Apr 2013 11:04:56 +0200] rev 51809
code tuning
blanchet [Mon, 29 Apr 2013 10:37:23 +0200] rev 51808
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
nipkow [Mon, 29 Apr 2013 11:31:40 +0200] rev 51807
tuned
traytel [Mon, 29 Apr 2013 10:03:35 +0200] rev 51806
tuned operator precedence
blanchet [Mon, 29 Apr 2013 09:45:14 +0200] rev 51805
use record instead of huge tuple
blanchet [Mon, 29 Apr 2013 09:10:49 +0200] rev 51804
renamed BNF "(co)data" commands to names that are closer to their final names
nipkow [Mon, 29 Apr 2013 06:13:36 +0200] rev 51803
tuned
nipkow [Mon, 29 Apr 2013 04:30:05 +0200] rev 51802
tuned
nipkow [Mon, 29 Apr 2013 04:20:42 +0200] rev 51801
tuned
nipkow [Sun, 28 Apr 2013 09:10:43 +0200] rev 51800
tuned
ballarin [Sat, 27 Apr 2013 21:56:45 +0200] rev 51799
Clarified confusing sentence in locales tutorial.
wenzelm [Sat, 27 Apr 2013 20:50:20 +0200] rev 51798
uniform Proof.context for hyp_subst_tac;
blanchet [Sat, 27 Apr 2013 11:37:50 +0200] rev 51797
tuned ML and thy file names
blanchet [Fri, 26 Apr 2013 14:16:05 +0200] rev 51796
merged
blanchet [Fri, 26 Apr 2013 14:14:55 +0200] rev 51795
for compatibility, generate recursor arguments in the same order as old package
blanchet [Fri, 26 Apr 2013 14:14:54 +0200] rev 51794
tuning in preparation for actual changes
blanchet [Fri, 26 Apr 2013 14:14:52 +0200] rev 51793
started working on compatibility with old package's recursor
nipkow [Fri, 26 Apr 2013 13:23:21 +0200] rev 51792
simplified def
nipkow [Fri, 26 Apr 2013 13:12:14 +0200] rev 51791
more standard argument order
blanchet [Fri, 26 Apr 2013 12:09:51 +0200] rev 51790
more intuitive syntax for equality-style discriminators of nullary constructors
blanchet [Fri, 26 Apr 2013 11:04:47 +0200] rev 51789
updated keywords
blanchet [Fri, 26 Apr 2013 11:04:46 +0200] rev 51788
put an underscore in prefix
blanchet [Fri, 26 Apr 2013 11:04:45 +0200] rev 51787
changed discriminator default: avoid mixing ctor and dtor views
nipkow [Fri, 26 Apr 2013 09:53:11 +0200] rev 51786
simplified def
nipkow [Fri, 26 Apr 2013 09:41:45 +0200] rev 51785
more standard order of arguments
nipkow [Fri, 26 Apr 2013 09:01:45 +0200] rev 51784
more funs
nipkow [Fri, 26 Apr 2013 07:49:38 +0200] rev 51783
simplified def
traytel [Thu, 25 Apr 2013 19:18:20 +0200] rev 51782
removed unnecessary assumptions in some theorems about cardinal exponentiation
blanchet [Thu, 25 Apr 2013 18:27:26 +0200] rev 51781
renamed "wrap_data" to "wrap_free_constructors"
blanchet [Thu, 25 Apr 2013 18:14:04 +0200] rev 51780
register coinductive type's coinduct rule
blanchet [Thu, 25 Apr 2013 17:25:10 +0200] rev 51779
compile
blanchet [Thu, 25 Apr 2013 17:13:24 +0200] rev 51778
adjusted stream library to coinduct attributes
blanchet [Thu, 25 Apr 2013 17:13:24 +0200] rev 51777
generate proper attributes for coinduction rules
wenzelm [Thu, 25 Apr 2013 13:22:45 +0200] rev 51776
updated to jdk-7u21;
hoelzl [Thu, 25 Apr 2013 11:59:21 +0200] rev 51775
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl [Thu, 25 Apr 2013 10:35:56 +0200] rev 51774
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
hoelzl [Wed, 24 Apr 2013 13:28:30 +0200] rev 51773
spell conditional_ly_-complete lattices correct
traytel [Thu, 25 Apr 2013 10:31:10 +0200] rev 51772
specify nicer names for map, set and rel in the stream library
blanchet [Thu, 25 Apr 2013 09:25:50 +0200] rev 51771
start making "wrap_data" more robust
blanchet [Thu, 25 Apr 2013 08:56:37 +0200] rev 51770
no eta-expansion for case in split rules and case_conv
blanchet [Thu, 25 Apr 2013 08:56:10 +0200] rev 51769
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
blanchet [Wed, 24 Apr 2013 22:48:22 +0200] rev 51768
proper error generated for wrong mixfix
blanchet [Wed, 24 Apr 2013 18:49:52 +0200] rev 51767
honor user-specified name for relator + generalize syntax
blanchet [Wed, 24 Apr 2013 17:47:22 +0200] rev 51766
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet [Wed, 24 Apr 2013 17:03:43 +0200] rev 51765
added "fundef_cong" attribute to "map_cong"
traytel [Wed, 24 Apr 2013 16:43:19 +0200] rev 51764
optimized proofs
blanchet [Wed, 24 Apr 2013 16:21:23 +0200] rev 51763
apply arguments to f and g in "case_cong"
blanchet [Wed, 24 Apr 2013 15:42:00 +0200] rev 51762
derive "map_cong"
blanchet [Wed, 24 Apr 2013 14:15:01 +0200] rev 51761
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet [Wed, 24 Apr 2013 14:14:36 +0200] rev 51760
killed dead code
blanchet [Wed, 24 Apr 2013 14:05:16 +0200] rev 51759
eta-contracted weak congruence rules (like in the old package)
blanchet [Wed, 24 Apr 2013 13:16:21 +0200] rev 51758
honor user-specified name for map function
blanchet [Wed, 24 Apr 2013 13:16:20 +0200] rev 51757
honor user-specified set function names
blanchet [Wed, 24 Apr 2013 13:16:20 +0200] rev 51756
parse set function name
nipkow [Wed, 24 Apr 2013 12:26:28 +0200] rev 51755
merged
nipkow [Wed, 24 Apr 2013 12:25:56 +0200] rev 51754
tuned
traytel [Wed, 24 Apr 2013 12:15:06 +0200] rev 51753
took out workaround for bug fixed in 5af40820948b
traytel [Wed, 24 Apr 2013 11:36:11 +0200] rev 51752
merged
traytel [Wed, 24 Apr 2013 11:06:53 +0200] rev 51751
slightly more aggressive syntax translation for printing case expressions
haftmann [Wed, 24 Apr 2013 11:32:54 +0200] rev 51750
avoid odd reinit after sublocale declaration
nipkow [Wed, 24 Apr 2013 10:23:47 +0200] rev 51749
moved defs into locale to reduce unnecessary polymorphism; tuned
haftmann [Tue, 23 Apr 2013 19:40:33 +0200] rev 51748
dropped dead code
haftmann [Tue, 23 Apr 2013 19:31:24 +0200] rev 51747
documentation and NEWS
blanchet [Tue, 23 Apr 2013 17:46:12 +0200] rev 51746
avoid accidental specialization of the types in the "map" property of codatatypes
blanchet [Tue, 23 Apr 2013 17:15:44 +0200] rev 51745
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet [Tue, 23 Apr 2013 17:13:14 +0200] rev 51744
more examples
blanchet [Tue, 23 Apr 2013 16:49:14 +0200] rev 51743
tuning
blanchet [Tue, 23 Apr 2013 16:41:59 +0200] rev 51742
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
blanchet [Tue, 23 Apr 2013 16:30:30 +0200] rev 51741
tuning
blanchet [Tue, 23 Apr 2013 16:30:29 +0200] rev 51740
tuned_comment
traytel [Tue, 23 Apr 2013 11:43:09 +0200] rev 51739
(co)rec is (just as the (un)fold) the unique morphism;
haftmann [Tue, 23 Apr 2013 11:14:51 +0200] rev 51738
tuned: unnamed contexts, interpretation and sublocale in locale target;
corrected slip in List.thy: setsum requires commmutativity
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51737
target-sensitive user-level commands interpretation and sublocale
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51736
ML interfaces for various kinds of interpretation
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51735
brittleness stamping for local theories
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51734
tuned
immler [Mon, 22 Apr 2013 18:39:12 +0200] rev 51733
removed type constraints
hoelzl [Mon, 22 Apr 2013 16:36:02 +0200] rev 51732
NEWS
haftmann [Sun, 21 Apr 2013 20:08:13 +0200] rev 51731
more sharing
haftmann [Sun, 21 Apr 2013 16:29:40 +0200] rev 51730
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
formal initialisation of theory target during interpretation;
prefer Local_Theory.notes_kind to register mixin equations during interpretation;
more uniformity between note_eqns_register and note_eqns_dependency
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51729
dropped unusued identifier
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51728
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51727
tuned for uniformity
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51726
reflection as official HOL tool
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51725
follow Isabelle spacing praxis more thoroughly
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51724
honour FIXMEs as far as feasible at the moment
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51723
combined reify_data.ML into reflection.ML;
attempt to establish a more accessible and more consistent terminology;
more ML code in ML file rather than setup theory;
ML slightly tuned wrt. Isabelle coding conventions
nipkow [Sat, 20 Apr 2013 20:57:49 +0200] rev 51722
proved termination for fun-based AI
nipkow [Sat, 20 Apr 2013 19:30:04 +0200] rev 51721
tuned
nipkow [Fri, 19 Apr 2013 12:04:57 +0200] rev 51720
tuned
wenzelm [Thu, 18 Apr 2013 21:31:24 +0200] rev 51719
merged
wenzelm [Thu, 18 Apr 2013 21:10:12 +0200] rev 51718
tuned signature;
wenzelm [Thu, 18 Apr 2013 17:07:01 +0200] rev 51717
simplifier uses proper Proof.context instead of historic type simpset;
nipkow [Thu, 18 Apr 2013 20:18:50 +0200] rev 51716
merged
nipkow [Thu, 18 Apr 2013 20:18:37 +0200] rev 51715
avoided map_of in def of fun_rep (but still needed for efficient code)
haftmann [Thu, 18 Apr 2013 18:57:02 +0200] rev 51714
spelling
haftmann [Thu, 18 Apr 2013 18:55:23 +0200] rev 51713
spelling
nipkow [Wed, 17 Apr 2013 21:23:35 +0200] rev 51712
tuned
nipkow [Wed, 17 Apr 2013 21:11:01 +0200] rev 51711
complete revision: finally got rid of annoying L-predicate
nipkow [Wed, 17 Apr 2013 20:53:26 +0200] rev 51710
moved leastness lemma
wenzelm [Tue, 16 Apr 2013 17:54:14 +0200] rev 51709
proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2);
speculative update for yap (untested);
hoelzl [Mon, 15 Apr 2013 22:51:55 +0200] rev 51708
use automatic type coerctions in Sqrt example
wenzelm [Mon, 15 Apr 2013 12:03:16 +0200] rev 51707
make SML/NJ happy;
blanchet [Mon, 15 Apr 2013 10:41:03 +0200] rev 51706
not all Nitpick 'constructors' are injective -- careful
kleing [Sun, 14 Apr 2013 21:54:45 +1000] rev 51705
added another definition snipped
wenzelm [Fri, 12 Apr 2013 17:56:51 +0200] rev 51704
actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
wenzelm [Fri, 12 Apr 2013 17:21:51 +0200] rev 51703
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm [Fri, 12 Apr 2013 17:02:55 +0200] rev 51702
removed historic comments;
wenzelm [Fri, 12 Apr 2013 15:30:38 +0200] rev 51701
tuned exceptions -- avoid composing error messages in low-level situations;
wenzelm [Fri, 12 Apr 2013 14:54:14 +0200] rev 51700
tuned signature;
tuned comments;
wenzelm [Fri, 12 Apr 2013 12:20:51 +0200] rev 51699
proper identifiers -- avoid crash of case translations;
nipkow [Fri, 12 Apr 2013 08:27:43 +0200] rev 51698
reduced duplication
traytel [Thu, 11 Apr 2013 16:58:54 +0200] rev 51697
do not add case translation syntax in rep_datatype compatibility mode
traytel [Thu, 11 Apr 2013 16:39:01 +0200] rev 51696
run type inference on input to wrap_data
traytel [Thu, 11 Apr 2013 16:03:11 +0200] rev 51695
installed case translations in BNF package
nipkow [Thu, 11 Apr 2013 15:10:22 +0200] rev 51694
tuned
wenzelm [Wed, 10 Apr 2013 21:46:28 +0200] rev 51693
more antiquotations;
wenzelm [Wed, 10 Apr 2013 21:20:35 +0200] rev 51692
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
wenzelm [Wed, 10 Apr 2013 20:58:01 +0200] rev 51691
updated keywords;
wenzelm [Wed, 10 Apr 2013 20:06:36 +0200] rev 51690
merged
wenzelm [Wed, 10 Apr 2013 19:14:47 +0200] rev 51689
merged
wenzelm [Wed, 10 Apr 2013 17:27:38 +0200] rev 51688
obsolete -- tools should refer to proper Proof.context;
wenzelm [Wed, 10 Apr 2013 17:17:16 +0200] rev 51687
discontinued obsolete ML antiquotation @{claset};
wenzelm [Wed, 10 Apr 2013 17:02:47 +0200] rev 51686
added ML antiquotation @{theory_context};
wenzelm [Wed, 10 Apr 2013 15:30:19 +0200] rev 51685
more standard module name Axclass (according to file name);
traytel [Wed, 10 Apr 2013 19:52:19 +0200] rev 51684
made SML/NJ happy
hoelzl [Wed, 10 Apr 2013 18:51:21 +0200] rev 51683
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
traytel [Wed, 10 Apr 2013 17:49:16 +0200] rev 51682
NEWS and CONTRIBUTORS
traytel [Wed, 10 Apr 2013 17:49:16 +0200] rev 51681
declaration attribute for case combinators
berghofe [Tue, 09 Apr 2013 18:27:49 +0200] rev 51680
Handle dummy patterns in parse translation rather than check phase
traytel [Sat, 06 Apr 2013 01:42:07 +0200] rev 51679
disallow coercions to interfere with case translations
traytel [Fri, 05 Apr 2013 22:08:42 +0200] rev 51678
allow redundant cases in the list comprehension translation
traytel [Fri, 05 Apr 2013 22:08:42 +0200] rev 51677
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
separate ML-interface function that is not recurring (strip_case)
traytel [Fri, 05 Apr 2013 22:08:42 +0200] rev 51676
tuned whitespace
berghofe [Thu, 04 Apr 2013 18:48:40 +0200] rev 51675
Use Type.raw_match instead of Sign.typ_match
traytel [Fri, 05 Apr 2013 22:08:42 +0200] rev 51674
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel [Tue, 22 Jan 2013 14:33:45 +0100] rev 51673
separate data used for case translation from the datatype package
berghofe [Tue, 22 Jan 2013 13:32:41 +0100] rev 51672
case translations performed in a separate check phase (with adjustments by traytel)
wenzelm [Wed, 10 Apr 2013 13:10:38 +0200] rev 51671
formal proof context for axclass proofs;
avoid global_simpset_of -- refer to simpset of proof context;
wenzelm [Wed, 10 Apr 2013 12:31:35 +0200] rev 51670
prefer local context;
wenzelm [Wed, 10 Apr 2013 12:24:43 +0200] rev 51669
proper proof context;
removed historic comments;
wenzelm [Wed, 10 Apr 2013 11:51:56 +0200] rev 51668
tuned;
wenzelm [Tue, 09 Apr 2013 21:39:55 +0200] rev 51667
merged
wenzelm [Tue, 09 Apr 2013 21:22:15 +0200] rev 51666
add command timings (like document command status);
wenzelm [Tue, 09 Apr 2013 21:14:00 +0200] rev 51665
tuned signature;
wenzelm [Tue, 09 Apr 2013 20:34:15 +0200] rev 51664
public Isabelle_Process.xml_cache (thread-safe);
cache derived status messages;
wenzelm [Tue, 09 Apr 2013 20:27:27 +0200] rev 51663
tuned signature;
wenzelm [Tue, 09 Apr 2013 20:16:52 +0200] rev 51662
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm [Tue, 09 Apr 2013 15:59:02 +0200] rev 51661
clarified protocol_message undefinedness;
wenzelm [Tue, 09 Apr 2013 15:40:34 +0200] rev 51660
quote by Alan Kay;
wenzelm [Tue, 09 Apr 2013 15:37:23 +0200] rev 51659
more accurate documentation;
wenzelm [Tue, 09 Apr 2013 15:29:25 +0200] rev 51658
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;
wenzelm [Tue, 09 Apr 2013 13:55:28 +0200] rev 51657
more accurate documentation of "(structure)" mixfix;
wenzelm [Tue, 09 Apr 2013 13:24:00 +0200] rev 51656
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
wenzelm [Tue, 09 Apr 2013 13:20:09 +0200] rev 51655
tuned comment;
wenzelm [Tue, 09 Apr 2013 12:56:26 +0200] rev 51654
just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm [Tue, 09 Apr 2013 12:29:36 +0200] rev 51653
tuned message;
blanchet [Tue, 09 Apr 2013 16:32:04 +0200] rev 51652
handle case clashes on Mac file system by encoding goal numbers
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51651
avoid duplicate "tcon_" names
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51650
smoothly handle cyclic graphs
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51649
compile + fixed naming convention
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51648
reverted accidental changes to theory file + updated wrt ML file
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51647
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51646
work on CASC LTB ISA exporter
blanchet [Tue, 09 Apr 2013 15:19:14 +0200] rev 51645
tuning
hoelzl [Tue, 09 Apr 2013 15:07:35 +0200] rev 51644
add continuous_on rules for products
hoelzl [Tue, 09 Apr 2013 14:13:13 +0200] rev 51643
fixed spelling
hoelzl [Tue, 09 Apr 2013 14:04:47 +0200] rev 51642
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl [Tue, 09 Apr 2013 14:04:41 +0200] rev 51641
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
wenzelm [Mon, 08 Apr 2013 21:01:59 +0200] rev 51640
improved printing of exception CTERM (see also d0f0f37ec346);
wenzelm [Mon, 08 Apr 2013 17:10:49 +0200] rev 51639
prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
wenzelm [Mon, 08 Apr 2013 16:06:54 +0200] rev 51638
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm [Mon, 08 Apr 2013 15:44:09 +0200] rev 51637
discontinued odd magic number, which was once used for performance measurements;
wenzelm [Mon, 08 Apr 2013 15:35:48 +0200] rev 51636
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm [Mon, 08 Apr 2013 14:28:37 +0200] rev 51635
merged
wenzelm [Mon, 08 Apr 2013 14:18:39 +0200] rev 51634
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
blanchet [Mon, 08 Apr 2013 14:16:00 +0200] rev 51633
try to preserve original linearization
blanchet [Mon, 08 Apr 2013 12:27:13 +0200] rev 51632
use somewhat lighter encoding
blanchet [Mon, 08 Apr 2013 12:11:06 +0200] rev 51631
robustness w.r.t. unknown arguments
nipkow [Sun, 07 Apr 2013 15:08:34 +0200] rev 51630
cleaned
nipkow [Sun, 07 Apr 2013 10:06:37 +0200] rev 51629
cleaned
nipkow [Sat, 06 Apr 2013 18:42:55 +0200] rev 51628
tuned
wenzelm [Fri, 05 Apr 2013 20:54:55 +0200] rev 51627
tuned signature -- agree with markup terminology;
wenzelm [Fri, 05 Apr 2013 20:43:43 +0200] rev 51626
unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
nipkow [Fri, 05 Apr 2013 18:31:35 +0200] rev 51625
tuned document
nipkow [Fri, 05 Apr 2013 15:13:25 +0200] rev 51624
tuned
haftmann [Thu, 04 Apr 2013 22:46:14 +0200] rev 51623
sup on multisets
haftmann [Thu, 04 Apr 2013 22:29:59 +0200] rev 51622
convenient induction rule
wenzelm [Thu, 04 Apr 2013 20:59:16 +0200] rev 51621
tuned README -- less buzzwords;
wenzelm [Thu, 04 Apr 2013 18:44:22 +0200] rev 51620
more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);
wenzelm [Thu, 04 Apr 2013 18:25:47 +0200] rev 51619
added missing file;
wenzelm [Thu, 04 Apr 2013 18:20:00 +0200] rev 51618
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm [Thu, 04 Apr 2013 18:06:48 +0200] rev 51617
tuned signature -- concentrate GUI tools;
wenzelm [Thu, 04 Apr 2013 17:58:47 +0200] rev 51616
tuned signature -- concentrate GUI tools;
wenzelm [Thu, 04 Apr 2013 17:47:28 +0200] rev 51615
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
tuned signature;
wenzelm [Thu, 04 Apr 2013 17:33:04 +0200] rev 51614
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm [Thu, 04 Apr 2013 17:16:51 +0200] rev 51613
tuned imports;
wenzelm [Thu, 04 Apr 2013 12:06:23 +0200] rev 51612
added var_position in analogy to longid_position, for typing reports on input;
avoid duplicate token var report;
nipkow [Thu, 04 Apr 2013 10:30:28 +0200] rev 51611
removed unnerving (esp in jedit) and pointless warning
nipkow [Thu, 04 Apr 2013 08:10:20 +0200] rev 51610
tuned
wenzelm [Wed, 03 Apr 2013 22:31:05 +0200] rev 51609
merged
wenzelm [Wed, 03 Apr 2013 22:30:25 +0200] rev 51608
tuned;
wenzelm [Wed, 03 Apr 2013 22:05:24 +0200] rev 51607
recover implicit thread position for status messages (cf. eca8acb42e4a);
wenzelm [Wed, 03 Apr 2013 21:48:43 +0200] rev 51606
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm [Wed, 03 Apr 2013 21:30:32 +0200] rev 51605
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
actually fork terminal proofs in interactive mode (amending 8707df0b0255);
wenzelm [Wed, 03 Apr 2013 20:56:08 +0200] rev 51604
updated comment to 46b90bbc370d;
wenzelm [Wed, 03 Apr 2013 20:38:50 +0200] rev 51603
recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);
wenzelm [Wed, 03 Apr 2013 16:45:14 +0200] rev 51602
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
wenzelm [Wed, 03 Apr 2013 13:58:00 +0200] rev 51601
tuned output -- less bullets;
haftmann [Wed, 03 Apr 2013 22:26:04 +0200] rev 51600
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann [Wed, 03 Apr 2013 22:26:04 +0200] rev 51599
optionalized very specific code setup for multisets
haftmann [Wed, 03 Apr 2013 10:15:43 +0200] rev 51598
generalized lemma fold_image thanks to Peter Lammich
wenzelm [Tue, 02 Apr 2013 20:19:38 +0200] rev 51597
tuned;
wenzelm [Tue, 02 Apr 2013 16:29:40 +0200] rev 51596
NEWS for 635562bc14ef;
wenzelm [Tue, 02 Apr 2013 11:41:50 +0200] rev 51595
more centralized command timing;
clarified old-style timing message;
blanchet [Tue, 02 Apr 2013 10:58:51 +0200] rev 51594
got rid of legacy smartness
nipkow [Mon, 01 Apr 2013 17:42:29 +0200] rev 51593
added lemma
wenzelm [Sat, 30 Mar 2013 18:24:33 +0100] rev 51592
merged
wenzelm [Sat, 30 Mar 2013 17:27:21 +0100] rev 51591
amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
wenzelm [Sat, 30 Mar 2013 17:13:21 +0100] rev 51590
more formal cong_name;
wenzelm [Sat, 30 Mar 2013 16:34:02 +0100] rev 51589
timing status for forked diagnostic commands;
wenzelm [Sat, 30 Mar 2013 16:16:24 +0100] rev 51588
tooltip of command keyword includes timing information;
wenzelm [Sat, 30 Mar 2013 16:15:26 +0100] rev 51587
more operations on Time, Timing;
haftmann [Fri, 29 Mar 2013 18:57:47 +0100] rev 51586
reverted slip introduced in f738e6dbd844
wenzelm [Sat, 30 Mar 2013 14:57:06 +0100] rev 51585
added 'print_defn_rules' command;
tuned;
wenzelm [Sat, 30 Mar 2013 13:40:19 +0100] rev 51584
more item markup;
tuned signature;
wenzelm [Sat, 30 Mar 2013 12:13:39 +0100] rev 51583
item markup for Proof_Context.pretty_fact;
tuned signature;
wenzelm [Sat, 30 Mar 2013 11:43:17 +0100] rev 51582
obsolete, cf. Proof_Context.print_syntax;
wenzelm [Fri, 29 Mar 2013 22:26:25 +0100] rev 51581
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm [Fri, 29 Mar 2013 22:14:27 +0100] rev 51580
Pretty.item markup for improved readability of lists of items;
wenzelm [Fri, 29 Mar 2013 22:13:02 +0100] rev 51579
tuned message;
haftmann [Fri, 29 Mar 2013 11:32:07 +0100] rev 51578
convenience check for vain instantiation
wenzelm [Fri, 29 Mar 2013 13:32:53 +0100] rev 51577
improved centering via strikethrough offset;
boehmes [Thu, 28 Mar 2013 23:44:43 +0100] rev 51576
re-generated SMT certificates
boehmes [Thu, 28 Mar 2013 23:44:41 +0100] rev 51575
new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code
wenzelm [Thu, 28 Mar 2013 22:42:18 +0100] rev 51574
ghost bullet via markup, which is painted as bar under text (normally space);
kleing [Thu, 28 Mar 2013 16:11:48 +0100] rev 51573
replace induction by hammer
wenzelm [Thu, 28 Mar 2013 15:47:03 +0100] rev 51572
merged
wenzelm [Thu, 28 Mar 2013 15:37:39 +0100] rev 51571
merged;
wenzelm [Thu, 28 Mar 2013 15:36:45 +0100] rev 51570
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm [Thu, 28 Mar 2013 15:00:27 +0100] rev 51569
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;
wenzelm [Thu, 28 Mar 2013 14:47:37 +0100] rev 51568
tuned;
wenzelm [Thu, 28 Mar 2013 14:01:56 +0100] rev 51567
proper default browser info for interactive mode, notably thy_deps;
nipkow [Thu, 28 Mar 2013 15:45:08 +0100] rev 51566
improved pretty printing for state set acom
ballarin [Wed, 27 Mar 2013 22:36:03 +0100] rev 51565
Improvements to the print_dependencies command.
wenzelm [Wed, 27 Mar 2013 21:25:33 +0100] rev 51564
discontinued obsolete parallel_proofs_reuse_timing;
wenzelm [Wed, 27 Mar 2013 21:13:02 +0100] rev 51563
merged
wenzelm [Wed, 27 Mar 2013 21:07:10 +0100] rev 51562
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
wenzelm [Wed, 27 Mar 2013 21:12:49 +0100] rev 51561
merged
wenzelm [Wed, 27 Mar 2013 20:57:05 +0100] rev 51560
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
wenzelm [Wed, 27 Mar 2013 19:32:44 +0100] rev 51559
tuned;
wenzelm [Wed, 27 Mar 2013 18:04:21 +0100] rev 51558
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm [Wed, 27 Mar 2013 17:58:07 +0100] rev 51557
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm [Wed, 27 Mar 2013 17:55:21 +0100] rev 51556
more liberal handling of skipped proofs;
wenzelm [Wed, 27 Mar 2013 17:53:29 +0100] rev 51555
explicit Toplevel.is_skipped_proof;
tuned;
wenzelm [Wed, 27 Mar 2013 16:46:52 +0100] rev 51554
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
wenzelm [Wed, 27 Mar 2013 16:38:25 +0100] rev 51553
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm [Wed, 27 Mar 2013 14:50:30 +0100] rev 51552
clarified Skip_Proof.cheat_tac: more standard tactic;
clarified Method.cheating: check quick_and_dirty when it is actually applied;
wenzelm [Wed, 27 Mar 2013 14:19:18 +0100] rev 51551
tuned signature and module arrangement;
wenzelm [Wed, 27 Mar 2013 14:08:03 +0100] rev 51550
tuned;
wenzelm [Wed, 27 Mar 2013 11:54:53 +0100] rev 51549
tuned GUI;
haftmann [Wed, 27 Mar 2013 10:55:05 +0100] rev 51548
centralized various multiset operations in theory multiset;
more conversions between multisets and lists respectively
haftmann [Tue, 26 Mar 2013 22:09:39 +0100] rev 51547
avoid odd foundational terms after interpretation;
more uniform code setup
haftmann [Tue, 26 Mar 2013 21:53:56 +0100] rev 51546
more uniform style for interpretation and sublocale declarations
wenzelm [Tue, 26 Mar 2013 20:55:21 +0100] rev 51545
merged
wenzelm [Tue, 26 Mar 2013 20:37:32 +0100] rev 51544
tuned session specification;
wenzelm [Tue, 26 Mar 2013 20:36:32 +0100] rev 51543
tuned proof;
wenzelm [Tue, 26 Mar 2013 20:02:02 +0100] rev 51542
tuned imports;
wenzelm [Tue, 26 Mar 2013 19:43:31 +0100] rev 51541
tuned proofs;
haftmann [Tue, 26 Mar 2013 20:49:57 +0100] rev 51540
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
wenzelm [Tue, 26 Mar 2013 15:10:28 +0100] rev 51539
merged
wenzelm [Tue, 26 Mar 2013 14:38:44 +0100] rev 51538
proper input event handling;
wenzelm [Tue, 26 Mar 2013 14:14:39 +0100] rev 51537
more standard imports;
wenzelm [Tue, 26 Mar 2013 14:05:08 +0100] rev 51536
more specific Entry painting;
ignore theories with all commands below threshold;
wenzelm [Tue, 26 Mar 2013 14:03:31 +0100] rev 51535
tuned;
wenzelm [Tue, 26 Mar 2013 12:40:51 +0100] rev 51534
mixed theory/command entries;
tuned;
wenzelm [Tue, 26 Mar 2013 11:26:13 +0100] rev 51533
dockable window for timing information;
kleing [Tue, 26 Mar 2013 13:54:24 +0100] rev 51532
no \FIXME macro for ProgProve (moved to book)
hoelzl [Tue, 26 Mar 2013 12:21:01 +0100] rev 51531
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl [Tue, 26 Mar 2013 12:21:00 +0100] rev 51530
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
hoelzl [Tue, 26 Mar 2013 12:21:00 +0100] rev 51529
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
hoelzl [Tue, 26 Mar 2013 12:20:59 +0100] rev 51528
Series.thy is based on Limits.thy and not Deriv.thy
hoelzl [Tue, 26 Mar 2013 12:20:59 +0100] rev 51527
move Ln.thy and Log.thy to Transcendental.thy
hoelzl [Tue, 26 Mar 2013 12:20:58 +0100] rev 51526
move SEQ.thy and Lim.thy to Limits.thy
hoelzl [Tue, 26 Mar 2013 12:20:58 +0100] rev 51525
HOL-NSA should only import Complex_Main
hoelzl [Tue, 26 Mar 2013 12:20:57 +0100] rev 51524
rename RealVector.thy to Real_Vector_Spaces.thy
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 51523
rename RealDef to Real
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 51522
remove Real.thy
hoelzl [Tue, 26 Mar 2013 12:20:55 +0100] rev 51521
merge RComplete into RealDef
hoelzl [Tue, 26 Mar 2013 12:20:54 +0100] rev 51520
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
hoelzl [Tue, 26 Mar 2013 12:20:53 +0100] rev 51519
remove posreal_complete
hoelzl [Tue, 26 Mar 2013 12:20:52 +0100] rev 51518
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
ballarin [Mon, 25 Mar 2013 20:00:27 +0100] rev 51517
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51516
Remove obsolete URLs in documentation of HOL-Algebra.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51515
Fix issue related to mixins in roundup.
Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.
kleing [Mon, 25 Mar 2013 15:18:44 +0100] rev 51514
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
nipkow [Mon, 25 Mar 2013 15:09:41 +0100] rev 51513
added lemmas
wenzelm [Mon, 25 Mar 2013 14:07:59 +0100] rev 51512
merged
wenzelm [Mon, 25 Mar 2013 14:04:01 +0100] rev 51511
clarified text_fold vs. fbrk;
wenzelm [Mon, 25 Mar 2013 13:37:44 +0100] rev 51510
tuned print_classes: more standard order, markup, formatting;
uniform printing of minimal supersort/classrel;
wenzelm [Mon, 25 Mar 2013 11:05:07 +0100] rev 51509
tuned message;
wenzelm [Mon, 25 Mar 2013 10:45:47 +0100] rev 51508
actually exit on scalac failure;
wenzelm [Mon, 25 Mar 2013 10:37:38 +0100] rev 51507
tuned signature;
kleing [Mon, 25 Mar 2013 13:50:50 +0100] rev 51506
removed obsolete uses of ext
wenzelm [Sun, 24 Mar 2013 16:19:54 +0100] rev 51505
prefer preset = 3 -- much faster and less memory requirement;
wenzelm [Sun, 24 Mar 2013 16:12:45 +0100] rev 51504
basic support for xz files;
wenzelm [Sun, 24 Mar 2013 16:10:19 +0100] rev 51503
added component xz-java-1.2;
wenzelm [Sun, 24 Mar 2013 14:26:10 +0100] rev 51502
more "quick start" hints;
more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle";
tuned;
traytel [Sun, 24 Mar 2013 12:07:31 +0100] rev 51501
simple case syntax for stream (stolen from AFP/Coinductive)
wenzelm [Sat, 23 Mar 2013 21:48:03 +0100] rev 51500
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
tuned proofs;
wenzelm [Sat, 23 Mar 2013 21:19:10 +0100] rev 51499
merged
wenzelm [Sat, 23 Mar 2013 21:13:03 +0100] rev 51498
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
wenzelm [Sat, 23 Mar 2013 19:54:15 +0100] rev 51497
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
wenzelm [Sat, 23 Mar 2013 19:39:31 +0100] rev 51496
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm [Sat, 23 Mar 2013 16:46:09 +0100] rev 51495
apply small result immediately, to avoid visible delay of text update after window move;
wenzelm [Sat, 23 Mar 2013 16:10:46 +0100] rev 51494
structural equality for Command.Results;
more general Command.State.eq_content;
wenzelm [Sat, 23 Mar 2013 13:57:46 +0100] rev 51493
allow fractional pretty margin -- avoid premature rounding;
wenzelm [Sat, 23 Mar 2013 13:12:39 +0100] rev 51492
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
wenzelm [Sat, 23 Mar 2013 13:04:28 +0100] rev 51491
tuned;
haftmann [Sat, 23 Mar 2013 20:57:57 +0100] rev 51490
spelling
haftmann [Sat, 23 Mar 2013 20:50:39 +0100] rev 51489
fundamental revision of big operators on sets
haftmann [Sat, 23 Mar 2013 17:11:06 +0100] rev 51488
tuned proof
haftmann [Sat, 23 Mar 2013 17:11:06 +0100] rev 51487
locales for abstract orders
krauss [Sat, 23 Mar 2013 07:30:53 +0100] rev 51486
merged
krauss [Fri, 22 Mar 2013 00:39:16 +0100] rev 51485
added rudimentary induction rule for partial_function (heap)
krauss [Fri, 22 Mar 2013 00:39:14 +0100] rev 51484
allow induction predicates with arbitrary arity (not just binary)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51483
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51482
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51481
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51480
move connected to HOL image; used to show intermediate value theorem
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51479
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51478
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51477
clean up lemma_nest_unique and renamed to nested_sequence_unique
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51476
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51475
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51474
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51473
move first_countable_topology to the HOL image
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51472
move metric_space to its own theory
hoelzl [Fri, 22 Mar 2013 10:41:42 +0100] rev 51471
move topological_space to its own theory
wenzelm [Thu, 21 Mar 2013 16:58:14 +0100] rev 51470
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm [Thu, 21 Mar 2013 16:35:53 +0100] rev 51469
eliminated char_width_int to avoid unclear rounding;
clarified integer conversion for margin;
nipkow [Thu, 21 Mar 2013 10:05:03 +0100] rev 51468
proofs depend only on constraints, not on def of L WHILE
blanchet [Wed, 20 Mar 2013 15:35:35 +0100] rev 51467
use the right role for SPASS hypotheses
kleing [Wed, 20 Mar 2013 14:56:30 +0100] rev 51466
soundness statement as in type system
kleing [Wed, 20 Mar 2013 11:32:16 +0100] rev 51465
add label for referencing in semantics book
nipkow [Wed, 20 Mar 2013 11:16:31 +0100] rev 51464
tuned
nipkow [Tue, 19 Mar 2013 21:35:15 +0100] rev 51463
get rid of xcolor warnings
traytel [Tue, 19 Mar 2013 15:59:58 +0100] rev 51462
extended stream library
kleing [Tue, 19 Mar 2013 14:04:53 +0100] rev 51461
export datatype definition which gets expanded too much in antiquotation
nipkow [Tue, 19 Mar 2013 14:07:13 +0100] rev 51460
tuned
Andreas Lochbihler [Tue, 19 Mar 2013 13:19:21 +0100] rev 51459
add induction rule for partial_function (tailrec)
wenzelm [Mon, 18 Mar 2013 20:02:37 +0100] rev 51458
prefer ownerless window, to avoid question of potentially changing parent view;
wenzelm [Mon, 18 Mar 2013 19:33:25 +0100] rev 51457
proper parent component for window.init;
kleing [Mon, 18 Mar 2013 19:20:53 +0100] rev 51456
lemma names and a corollary
kleing [Mon, 18 Mar 2013 14:47:20 +0100] rev 51455
managed to eliminate further snippets
kleing [Mon, 18 Mar 2013 14:27:38 +0100] rev 51454
fewer IMP snippets
wenzelm [Mon, 18 Mar 2013 13:18:42 +0100] rev 51453
merged
wenzelm [Mon, 18 Mar 2013 11:29:50 +0100] rev 51452
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm [Mon, 18 Mar 2013 11:04:59 +0100] rev 51451
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
wenzelm [Sun, 17 Mar 2013 22:02:06 +0100] rev 51450
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm [Sun, 17 Mar 2013 21:04:38 +0100] rev 51449
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
nipkow [Mon, 18 Mar 2013 12:31:13 +0100] rev 51448
tuned
traytel [Mon, 18 Mar 2013 11:25:24 +0100] rev 51447
eliminate duplicated constant (diag vs. Id_on)
traytel [Mon, 18 Mar 2013 11:05:33 +0100] rev 51446
hide internal constants; tuned proofs
nipkow [Mon, 18 Mar 2013 10:28:42 +0100] rev 51445
tuned
nipkow [Sun, 17 Mar 2013 20:29:26 +0100] rev 51444
tuned
nipkow [Sun, 17 Mar 2013 20:27:13 +0100] rev 51443
added advanced rule induction subsection
wenzelm [Sat, 16 Mar 2013 21:44:04 +0100] rev 51442
merged
wenzelm [Sat, 16 Mar 2013 21:26:44 +0100] rev 51441
more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm [Sat, 16 Mar 2013 17:16:39 +0100] rev 51440
some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;
wenzelm [Sat, 16 Mar 2013 12:46:22 +0100] rev 51439
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors);
early initialization of gutter to get proper text area painter size (see also 2585c81d840a);
kuncar [Sat, 16 Mar 2013 20:51:47 +0100] rev 51438
drop a workaround because of 8739f8abbecb
kuncar [Sat, 16 Mar 2013 20:51:23 +0100] rev 51437
fixing transfer tactic - unfold fully identity relation by using relator_eq
nipkow [Sat, 16 Mar 2013 17:22:05 +0100] rev 51436
tuned (in particular bold fonts)
wenzelm [Sat, 16 Mar 2013 10:50:23 +0100] rev 51435
merged
wenzelm [Thu, 14 Mar 2013 16:49:36 +0100] rev 51434
document ISABELLE_POLYML;
nipkow [Fri, 15 Mar 2013 18:49:40 +0100] rev 51433
tuned
wenzelm [Fri, 15 Mar 2013 13:46:37 +0100] rev 51432
simplified time_CPU and time_GC;
derive relative speed from time (considered as step function);
wenzelm [Fri, 15 Mar 2013 10:49:28 +0100] rev 51431
updated to scala-2.10.1;
traytel [Fri, 15 Mar 2013 10:08:23 +0100] rev 51430
extended stream library (sdrop_while)
wenzelm [Thu, 14 Mar 2013 14:25:55 +0100] rev 51429
tuned signature;
wenzelm [Thu, 14 Mar 2013 14:14:58 +0100] rev 51428
more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;
wenzelm [Thu, 14 Mar 2013 13:57:44 +0100] rev 51427
proper use of "member", without embarking on delicate questions about SML equality types;
wenzelm [Thu, 14 Mar 2013 13:52:22 +0100] rev 51426
made SML/NJ happy;
nipkow [Thu, 14 Mar 2013 10:51:28 +0100] rev 51425
tuned
wenzelm [Wed, 13 Mar 2013 22:46:28 +0100] rev 51424
merged
wenzelm [Wed, 13 Mar 2013 21:25:08 +0100] rev 51423
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;
wenzelm [Wed, 13 Mar 2013 17:15:25 +0100] rev 51422
proper formatting, to facilitate line-based diff;
wenzelm [Wed, 13 Mar 2013 17:13:22 +0100] rev 51421
more uniform session descriptions, which show up in chapter index;
wenzelm [Wed, 13 Mar 2013 17:06:45 +0100] rev 51420
proper index for HOL-Proofs, which is also in chapter "HOL";
wenzelm [Wed, 13 Mar 2013 16:57:05 +0100] rev 51419
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
wenzelm [Wed, 13 Mar 2013 16:04:16 +0100] rev 51418
more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
wenzelm [Wed, 13 Mar 2013 15:12:14 +0100] rev 51417
sessions may be organized via 'chapter' in ROOT;
wenzelm [Wed, 13 Mar 2013 15:08:38 +0100] rev 51416
do not absorb I/O errors;
wenzelm [Wed, 13 Mar 2013 14:57:16 +0100] rev 51415
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
paulson [Wed, 13 Mar 2013 17:17:33 +0000] rev 51414
new lemma subset_decode_imp_le
kleing [Wed, 13 Mar 2013 16:03:55 +0100] rev 51413
merged
kleing [Wed, 13 Mar 2013 16:03:40 +0100] rev 51412
more IMP snippets
kuncar [Wed, 13 Mar 2013 14:33:15 +0100] rev 51411
rename fset_member to fmember and prove parametricity
traytel [Wed, 13 Mar 2013 13:23:16 +0100] rev 51410
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel [Wed, 13 Mar 2013 10:47:00 +0100] rev 51409
nitpick setup and code generation for streams
nipkow [Wed, 13 Mar 2013 10:15:01 +0100] rev 51408
merged
nipkow [Wed, 13 Mar 2013 10:14:50 +0100] rev 51407
tuned
wenzelm [Tue, 12 Mar 2013 22:44:03 +0100] rev 51406
proper path -- I/O was hidden due to permissiveness;
wenzelm [Tue, 12 Mar 2013 22:24:01 +0100] rev 51405
merged
wenzelm [Tue, 12 Mar 2013 22:22:05 +0100] rev 51404
removed odd cvs artifacts;
wenzelm [Tue, 12 Mar 2013 21:59:48 +0100] rev 51403
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm [Tue, 12 Mar 2013 20:03:04 +0100] rev 51402
include session description in chapter index;
prefer alphabetical order;
wenzelm [Tue, 12 Mar 2013 18:44:48 +0100] rev 51401
tuned;
wenzelm [Tue, 12 Mar 2013 18:30:28 +0100] rev 51400
more accurate theory links;
wenzelm [Tue, 12 Mar 2013 16:47:24 +0100] rev 51399
discontinued "isabelle usedir" option -r (reset session path);
simplified internal session identification: chapter / name;
clarified chapter index (of sessions) vs. session index (of theories);
discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser);
removed obsolete session parent_path;
wenzelm [Mon, 11 Mar 2013 14:25:14 +0100] rev 51398
discontinued "isabelle usedir" option -P (remote path);
wenzelm [Mon, 11 Mar 2013 13:28:46 +0100] rev 51397
support for 'chapter' specifications within session ROOT;
nipkow [Tue, 12 Mar 2013 19:55:17 +0100] rev 51396
added latex markup
kleing [Tue, 12 Mar 2013 11:59:26 +0100] rev 51395
merged
kleing [Tue, 12 Mar 2013 11:59:02 +0100] rev 51394
more snippets
nipkow [Tue, 12 Mar 2013 11:31:31 +0100] rev 51393
added pairs
nipkow [Tue, 12 Mar 2013 07:51:10 +0100] rev 51392
extended set comprehension notation with {pttrn : A . P}
nipkow [Mon, 11 Mar 2013 18:33:21 +0100] rev 51391
tuned
nipkow [Mon, 11 Mar 2013 12:27:31 +0100] rev 51390
more factorisation of Step & Co
nipkow [Sun, 10 Mar 2013 18:29:10 +0100] rev 51389
factored out Step
nipkow [Sun, 10 Mar 2013 14:36:18 +0100] rev 51388
merged
nipkow [Sun, 10 Mar 2013 14:36:03 +0100] rev 51387
stepwise instantiation is more modular
haftmann [Sun, 10 Mar 2013 11:21:16 +0100] rev 51386
generalized subclass relation;
tuned proof
nipkow [Sun, 10 Mar 2013 10:10:01 +0100] rev 51385
termination proof for narrowing: fewer assumptions
wenzelm [Sat, 09 Mar 2013 18:22:20 +0100] rev 51384
accomodate encrypted file-system on linux;
wenzelm [Sat, 09 Mar 2013 13:01:24 +0100] rev 51383
tuned;
haftmann [Sat, 09 Mar 2013 11:56:01 +0100] rev 51382
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
wenzelm [Fri, 08 Mar 2013 17:19:27 +0100] rev 51381
updated keywords (cf. 84d01fd733cf);
blanchet [Fri, 08 Mar 2013 14:15:39 +0100] rev 51380
proper type inference for default values
kuncar [Fri, 08 Mar 2013 13:21:58 +0100] rev 51379
convert mappings to parametric lifting
kuncar [Fri, 08 Mar 2013 13:21:55 +0100] rev 51378
setup_lifting doesn't support a type variable as a raw type
kuncar [Fri, 08 Mar 2013 13:21:52 +0100] rev 51377
add [relator_mono] and [relator_distr] rules
kuncar [Fri, 08 Mar 2013 13:21:45 +0100] rev 51376
simplify Lift_FSet because we have parametricity in Lifting now
kuncar [Fri, 08 Mar 2013 13:21:06 +0100] rev 51375
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar [Fri, 08 Mar 2013 13:14:23 +0100] rev 51374
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
nipkow [Fri, 08 Mar 2013 11:28:20 +0100] rev 51373
merged
nipkow [Fri, 08 Mar 2013 11:28:04 +0100] rev 51372
simplified basic termination proof
traytel [Fri, 08 Mar 2013 09:34:38 +0100] rev 51371
some simp rules for fset
wenzelm [Thu, 07 Mar 2013 18:14:30 +0100] rev 51370
avoid -Infinity which confuses JFreeChart histogram;
wenzelm [Thu, 07 Mar 2013 17:50:26 +0100] rev 51369
tuned proofs -- more structure, less warnings;
wenzelm [Thu, 07 Mar 2013 15:02:55 +0100] rev 51368
tuned signature -- prefer terminology of Scala and Axiom;
blanchet [Thu, 07 Mar 2013 13:44:54 +0100] rev 51367
better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
huffman [Wed, 06 Mar 2013 10:44:43 -0800] rev 51366
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51365
netlimit is abbreviation for Lim
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51364
tuned proofs
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51363
changed has_derivative_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51362
changed continuous_on_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51361
changed continuous_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 51360
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
nipkow [Wed, 06 Mar 2013 16:10:56 +0100] rev 51359
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow [Wed, 06 Mar 2013 14:10:07 +0100] rev 51358
added lemma
nipkow [Wed, 06 Mar 2013 12:17:52 +0100] rev 51357
extended numerals
wenzelm [Tue, 05 Mar 2013 17:25:41 +0100] rev 51356
merged
wenzelm [Tue, 05 Mar 2013 17:07:36 +0100] rev 51355
merged
wenzelm [Tue, 05 Mar 2013 11:37:01 +0100] rev 51354
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
traytel [Tue, 05 Mar 2013 17:18:02 +0100] rev 51353
extended stream library a little more
traytel [Tue, 05 Mar 2013 17:10:49 +0100] rev 51352
extended stream library
hoelzl [Tue, 05 Mar 2013 15:43:22 +0100] rev 51351
generalized lemmas in Extended_Real_Limits
hoelzl [Tue, 05 Mar 2013 15:43:21 +0100] rev 51350
eventually nhds represented using sequentially
hoelzl [Tue, 05 Mar 2013 15:43:20 +0100] rev 51349
generalized compact_Times to topological_space
hoelzl [Tue, 05 Mar 2013 15:43:19 +0100] rev 51348
move lemma Inf to usage point
hoelzl [Tue, 05 Mar 2013 15:43:18 +0100] rev 51347
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
hoelzl [Tue, 05 Mar 2013 15:43:17 +0100] rev 51346
tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
hoelzl [Tue, 05 Mar 2013 15:43:16 +0100] rev 51345
generalized continuous/compact_attains_inf/sup from real to linorder_topology
hoelzl [Tue, 05 Mar 2013 15:43:15 +0100] rev 51344
continuity of pair operations
hoelzl [Tue, 05 Mar 2013 15:43:14 +0100] rev 51343
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl [Tue, 05 Mar 2013 15:43:13 +0100] rev 51342
generalized isGlb_unique
hoelzl [Tue, 05 Mar 2013 15:43:12 +0100] rev 51341
complete_linorder is also a complete_distrib_lattice
hoelzl [Tue, 05 Mar 2013 15:43:08 +0100] rev 51340
move Liminf / Limsup lemmas on complete_lattices to its own file
nipkow [Tue, 05 Mar 2013 15:27:08 +0100] rev 51339
merged
nipkow [Tue, 05 Mar 2013 15:26:57 +0100] rev 51338
New theory of infinity-extended types; should replace Extended_xyz eventually
webertj [Tue, 05 Mar 2013 13:03:24 +0100] rev 51337
Avoid ML warning about unreferenced identifier.
blanchet [Tue, 05 Mar 2013 11:59:58 +0100] rev 51336
polymorphic SPASS is also SPASS
traytel [Tue, 05 Mar 2013 09:47:15 +0100] rev 51335
allow more general coercion maps; tuned;
nipkow [Tue, 05 Mar 2013 10:16:15 +0100] rev 51334
more lemmas about intervals
wenzelm [Mon, 04 Mar 2013 17:32:10 +0100] rev 51333
merged
wenzelm [Mon, 04 Mar 2013 15:03:46 +0100] rev 51332
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
wenzelm [Mon, 04 Mar 2013 11:36:16 +0100] rev 51331
join all proofs before scheduling present phase (ordered according to weight);
tuned;
wenzelm [Mon, 04 Mar 2013 10:02:58 +0100] rev 51330
more explicit datatype result;
hoelzl [Wed, 20 Feb 2013 12:04:42 +0100] rev 51329
split dense into inner_dense_order and no_top/no_bot
hoelzl [Wed, 20 Feb 2013 12:04:42 +0100] rev 51328
move auxiliary lemmas from Library/Extended_Reals to HOL image
traytel [Mon, 04 Mar 2013 09:57:54 +0100] rev 51327
tuned (extend datatype to inline option)
wenzelm [Sun, 03 Mar 2013 18:50:46 +0100] rev 51326
prefer more systematic Future.flat;
wenzelm [Sun, 03 Mar 2013 17:34:42 +0100] rev 51325
more uniform Future.map: always internalize failure;
added Future.flat as fast-path operation;
wenzelm [Sun, 03 Mar 2013 14:29:30 +0100] rev 51324
uniform treatment of global/local proofs;
tuned;
wenzelm [Sun, 03 Mar 2013 13:57:03 +0100] rev 51323
tuned;
wenzelm [Sun, 03 Mar 2013 13:43:57 +0100] rev 51322
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
wenzelm [Sun, 03 Mar 2013 13:23:06 +0100] rev 51321
more Thy_Syntax.element operations;
traytel [Fri, 01 Mar 2013 22:15:31 +0100] rev 51320
coercion-invariant arguments at work
traytel [Fri, 01 Mar 2013 22:15:31 +0100] rev 51319
constants with coercion-invariant arguments (possibility to disable/reenable
coercions under certain constants, necessary for the forthcoming logically
unspecified control structures for case translations)
wenzelm [Thu, 28 Feb 2013 21:11:07 +0100] rev 51318
simplified Proof.future_proof;
wenzelm [Thu, 28 Feb 2013 18:35:31 +0100] rev 51317
provide explicit dummy names (cf. dfe469293eb4);
wenzelm [Thu, 28 Feb 2013 17:38:35 +0100] rev 51316
discontinued empty name bindings in 'axiomatization';
wenzelm [Thu, 28 Feb 2013 17:14:55 +0100] rev 51315
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm [Thu, 28 Feb 2013 16:54:52 +0100] rev 51314
just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;
wenzelm [Thu, 28 Feb 2013 16:38:17 +0100] rev 51313
discontinued obsolete 'axioms' command;
wenzelm [Thu, 28 Feb 2013 16:19:08 +0100] rev 51312
more robust build error handling, e.g. missing outer syntax commands;
wenzelm [Thu, 28 Feb 2013 14:29:54 +0100] rev 51311
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 14:24:21 +0100] rev 51310
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 14:22:14 +0100] rev 51309
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 14:10:54 +0100] rev 51308
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 13:54:45 +0100] rev 51307
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 13:46:45 +0100] rev 51306
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 13:33:01 +0100] rev 51305
eliminated legacy 'axioms';
wenzelm [Thu, 28 Feb 2013 13:24:51 +0100] rev 51304
marginalized historic strip_tac;
wenzelm [Thu, 28 Feb 2013 13:19:25 +0100] rev 51303
tuned proof;
wenzelm [Thu, 28 Feb 2013 12:43:28 +0100] rev 51302
tuned whitespace and indentation;
wenzelm [Thu, 28 Feb 2013 12:24:24 +0100] rev 51301
simplified imports;
wenzelm [Thu, 28 Feb 2013 12:09:32 +0100] rev 51300
load timings in parallel for improved performance;
wenzelm [Thu, 28 Feb 2013 11:40:23 +0100] rev 51299
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
wenzelm [Wed, 27 Feb 2013 20:36:21 +0100] rev 51298
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm [Wed, 27 Feb 2013 19:39:16 +0100] rev 51297
eliminated pointless re-ified errors;
wenzelm [Wed, 27 Feb 2013 17:44:08 +0100] rev 51296
merged
wenzelm [Wed, 27 Feb 2013 17:32:17 +0100] rev 51295
discontinued redundant 'use' command;
wenzelm [Wed, 27 Feb 2013 16:27:44 +0100] rev 51294
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm [Wed, 27 Feb 2013 12:45:19 +0100] rev 51293
discontinued obsolete 'uses' within theory header;
Andreas Lochbihler [Wed, 27 Feb 2013 13:48:15 +0100] rev 51292
use lemma from Big_Operators
Andreas Lochbihler [Wed, 27 Feb 2013 13:44:19 +0100] rev 51291
add inclusion/exclusion lemma
Andreas Lochbihler [Wed, 27 Feb 2013 13:43:04 +0100] rev 51290
added lemma
Andreas Lochbihler [Wed, 27 Feb 2013 10:33:45 +0100] rev 51289
merged
Andreas Lochbihler [Wed, 27 Feb 2013 10:33:30 +0100] rev 51288
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
wenzelm [Tue, 26 Feb 2013 20:11:11 +0100] rev 51287
updated Toplevel.command_exception;
wenzelm [Tue, 26 Feb 2013 20:09:25 +0100] rev 51286
tuned;
wenzelm [Tue, 26 Feb 2013 19:58:27 +0100] rev 51285
tuned signature;