| Tue, 11 Aug 2009 10:46:11 +0200 |
haftmann |
dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML
|
changeset |
files
|
| Tue, 11 Aug 2009 10:43:43 +0200 |
haftmann |
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
|
changeset |
files
|
| Tue, 11 Aug 2009 10:05:53 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 11 Aug 2009 10:05:16 +0200 |
haftmann |
temporary adjustment to dubious state of eta expansion in recfun_codegen
|
changeset |
files
|
| Mon, 10 Aug 2009 13:34:50 +0200 |
haftmann |
properly merged
|
changeset |
files
|
| Mon, 10 Aug 2009 12:25:30 +0200 |
haftmann |
same_typscheme replaces ugly common_typ_eqns
|
changeset |
files
|
| Mon, 10 Aug 2009 12:24:49 +0200 |
haftmann |
moved all technical processing of code equations to code_thingol.ML
|
changeset |
files
|
| Mon, 10 Aug 2009 12:24:47 +0200 |
haftmann |
added map_transpose
|
changeset |
files
|
| Mon, 10 Aug 2009 10:25:00 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 10 Aug 2009 08:37:37 +0200 |
haftmann |
attempt to move desymbolization to translation
|
changeset |
files
|
| Fri, 31 Jul 2009 10:49:09 +0200 |
haftmann |
added a somehow clueless comment
|
changeset |
files
|
| Fri, 31 Jul 2009 10:49:08 +0200 |
haftmann |
repair mess produced by resolution afterwards
|
changeset |
files
|
| Fri, 31 Jul 2009 09:46:09 +0200 |
haftmann |
using certify_instantiate
|
changeset |
files
|
| Fri, 31 Jul 2009 09:34:21 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 31 Jul 2009 09:34:05 +0200 |
haftmann |
cleaned up variable desymbolification and argument expansion
|
changeset |
files
|
| Thu, 30 Jul 2009 15:21:31 +0200 |
haftmann |
more appropriate printing of function terms
|
changeset |
files
|
| Thu, 30 Jul 2009 15:21:18 +0200 |
haftmann |
improved handling of parameters
|
changeset |
files
|
| Thu, 30 Jul 2009 15:20:57 +0200 |
haftmann |
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
|
changeset |
files
|
| Thu, 30 Jul 2009 13:52:18 +0200 |
haftmann |
towards proper handling of argument order in comprehensions
|
changeset |
files
|
| Thu, 30 Jul 2009 13:52:18 +0200 |
haftmann |
cleaned up
|
changeset |
files
|
| Thu, 30 Jul 2009 13:52:17 +0200 |
haftmann |
termT and term_of_const
|
changeset |
files
|
| Mon, 10 Aug 2009 18:12:55 +0200 |
nipkow |
added bij lemmas
|
changeset |
files
|
| Mon, 10 Aug 2009 17:00:41 +0200 |
nipkow |
new lemma bij_comp
|
changeset |
files
|
| Sat, 08 Aug 2009 11:40:22 +0200 |
wenzelm |
refined mac-poly64 tests;
|
changeset |
files
|
| Fri, 07 Aug 2009 19:16:04 +0200 |
wenzelm |
tuned spacing of sections;
|
changeset |
files
|
| Thu, 06 Aug 2009 22:30:27 +0200 |
wenzelm |
more platforms;
|
changeset |
files
|
| Thu, 06 Aug 2009 20:46:33 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Thu, 06 Aug 2009 19:51:59 +0200 |
wenzelm |
misc changes to SOS by Philipp Meyer:
|
changeset |
files
|
| Wed, 05 Aug 2009 17:10:10 +0200 |
wenzelm |
settings for ATP_Manager component;
|
changeset |
files
|
| Wed, 05 Aug 2009 16:17:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 05 Aug 2009 15:39:34 +0200 |
wenzelm |
SUBPROOF: recovered Goal.check_finished;
|
changeset |
files
|
| Tue, 04 Aug 2009 23:25:00 +0200 |
wenzelm |
added Isabelle_System.components;
|
changeset |
files
|
| Tue, 04 Aug 2009 19:20:24 +0200 |
wenzelm |
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
|
changeset |
files
|
| Tue, 04 Aug 2009 16:13:16 +0200 |
wenzelm |
etc/components;
|
changeset |
files
|
| Tue, 04 Aug 2009 16:11:11 +0200 |
wenzelm |
turned object-logics into components;
|
changeset |
files
|
| Tue, 04 Aug 2009 16:09:46 +0200 |
wenzelm |
spelling;
|
changeset |
files
|
| Tue, 04 Aug 2009 15:59:57 +0200 |
wenzelm |
tuned "Bootstrapping the environment";
|
changeset |
files
|
| Tue, 04 Aug 2009 15:05:34 +0200 |
wenzelm |
change IFS only locally -- thanks to bash arrays;
|
changeset |
files
|
| Tue, 04 Aug 2009 13:35:33 +0200 |
wenzelm |
more uniform handling of ISABELLE_HOME_USER component;
|
changeset |
files
|
| Tue, 04 Aug 2009 13:29:52 +0200 |
wenzelm |
options for more precise performance figures of at-poly, which happens to run on macbroy21;
|
changeset |
files
|
| Tue, 04 Aug 2009 08:45:03 +0200 |
bulwahn |
removing tracing messages in predicate compiler
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
commented rpred compilation; tuned
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
tuned proof procedure; added size-limiting predicate compilation of higher order predicates; added guessing of number parameters for registrating predicates; removed debug messages
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
changed resolving depending predicates and fetching in the predicate compiler
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
refactoring predicate compiler; repaired proof procedure to handle all test cases
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
refactoring predicate compiler; added type synonyms and functions split_smode and split_mode
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
imported patch changed mode inference of predicate compiler to return infered dataflow
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
imported patch generic compilation of predicate compiler with different monads
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory
|
changeset |
files
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
|
changeset |
files
|
| Tue, 04 Aug 2009 01:01:23 +0200 |
wenzelm |
basic support for components (which imitate the usual Isabelle directory layout);
|
changeset |
files
|
| Sun, 02 Aug 2009 21:03:38 +0200 |
berghofe |
Tuned.
|
changeset |
files
|
| Sun, 02 Aug 2009 17:58:19 +0200 |
Christian Urban |
the derived induction principles can be given an explicit name
|
changeset |
files
|
| Sat, 01 Aug 2009 20:34:34 +0200 |
wenzelm |
updated Variable.import;
|
changeset |
files
|
| Sat, 01 Aug 2009 00:39:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 01 Aug 2009 00:39:45 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 31 Jul 2009 11:34:14 +0200 |
wenzelm |
modernized generated example session;
|
changeset |
files
|
| Fri, 31 Jul 2009 23:31:11 +0200 |
boehmes |
added Mirabelle
|
changeset |
files
|
| Fri, 31 Jul 2009 23:30:21 +0200 |
boehmes |
Quickcheck callable from ML
|
changeset |
files
|
| Sat, 01 Aug 2009 00:17:03 +0200 |
wenzelm |
future scheduler: uninterruptible cancelation;
|
changeset |
files
|
| Sat, 01 Aug 2009 00:09:45 +0200 |
wenzelm |
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:50:11 +0200 |
wenzelm |
recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:37:53 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:23:52 +0200 |
wenzelm |
ISABELLE_USEDIR_OPTIONS: -q 2 by default;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:09:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Jul 2009 21:27:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Jul 2009 08:18:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 16:54:20 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
changeset |
files
|
| Wed, 29 Jul 2009 16:48:34 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
changeset |
files
|
| Thu, 30 Jul 2009 23:06:06 +0200 |
wenzelm |
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
|
changeset |
files
|
| Thu, 30 Jul 2009 18:43:52 +0200 |
wenzelm |
trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
|
changeset |
files
|
| Thu, 30 Jul 2009 17:54:57 +0200 |
wenzelm |
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
|
changeset |
files
|
| Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
changeset |
files
|
| Thu, 30 Jul 2009 11:23:57 +0200 |
wenzelm |
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
|
changeset |
files
|
| Thu, 30 Jul 2009 11:23:17 +0200 |
wenzelm |
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
|
changeset |
files
|
| Thu, 30 Jul 2009 01:14:40 +0200 |
wenzelm |
Variable.importT/import: return full instantiations, tuned;
|
changeset |
files
|
| Thu, 30 Jul 2009 01:12:33 +0200 |
wenzelm |
added certify_inst, certify_instantiate;
|
changeset |
files
|
| Wed, 29 Jul 2009 22:38:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 22:34:31 +0200 |
wenzelm |
trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
|
changeset |
files
|
| Wed, 29 Jul 2009 21:40:04 +0200 |
wenzelm |
proper Jinja-Slicing;
|
changeset |
files
|
| Wed, 29 Jul 2009 19:36:22 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 16:43:02 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
abstractions: desymbolize name hint
|
changeset |
files
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
added numeral code postprocessor rules on type int
|
changeset |
files
|
| Wed, 29 Jul 2009 12:13:21 +0200 |
nipkow |
sos comments modified
|
changeset |
files
|
| Wed, 29 Jul 2009 12:12:01 +0200 |
nipkow |
sos documentation
|
changeset |
files
|
| Wed, 29 Jul 2009 09:06:49 +0200 |
nipkow |
Added remote-SOS changes by Philipp Meyer
|
changeset |
files
|
| Fri, 24 Jul 2009 13:56:02 +0200 |
Philipp Meyer |
Functionality for sum of squares to call a remote csdp prover
|
changeset |
files
|
| Tue, 28 Jul 2009 20:26:39 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 28 Jul 2009 13:38:13 +0200 |
haftmann |
updated generated document
|
changeset |
files
|
| Tue, 28 Jul 2009 13:37:40 +0200 |
haftmann |
reinserted legacy ML function
|
changeset |
files
|
| Tue, 28 Jul 2009 13:37:09 +0200 |
haftmann |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
changeset |
files
|
| Tue, 28 Jul 2009 13:37:08 +0200 |
haftmann |
explicit is better than implicit
|
changeset |
files
|
| Wed, 29 Jul 2009 19:35:10 +0200 |
wenzelm |
Meson.first_order_resolve: avoid handle _;
|
changeset |
files
|
| Wed, 29 Jul 2009 00:09:14 +0200 |
wenzelm |
removed old global get_claset/map_claset;
|
changeset |
files
|
| Tue, 28 Jul 2009 20:03:58 +0200 |
wenzelm |
eliminated METAHYPS;
|
changeset |
files
|
| Tue, 28 Jul 2009 19:49:42 +0200 |
wenzelm |
Future.shutdown before loading sequentially -- workaround scheduler deadlock;
|
changeset |
files
|
| Tue, 28 Jul 2009 18:17:36 +0200 |
wenzelm |
ResAxioms.neg_conjecture_clauses: proper context;
|
changeset |
files
|
| Tue, 28 Jul 2009 18:17:35 +0200 |
wenzelm |
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
|
changeset |
files
|
| Tue, 28 Jul 2009 18:17:35 +0200 |
wenzelm |
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
|
changeset |
files
|
| Tue, 28 Jul 2009 16:30:23 +0200 |
wenzelm |
eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
|
changeset |
files
|
| Tue, 28 Jul 2009 16:28:49 +0200 |
wenzelm |
non-critical use_thy;
|
changeset |
files
|
| Tue, 28 Jul 2009 15:10:15 +0200 |
wenzelm |
future result: Synchronized.var;
|
changeset |
files
|
| Tue, 28 Jul 2009 15:05:18 +0200 |
wenzelm |
added unsynchronized Synchronized.peek;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:54:53 +0200 |
wenzelm |
group status: Synchronized.var;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:43:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:35:27 +0200 |
wenzelm |
Task_Queue.dequeue: explicit thread;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:29:25 +0200 |
wenzelm |
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:11:15 +0200 |
wenzelm |
interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
|
changeset |
files
|
| Tue, 28 Jul 2009 14:04:33 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Tue, 28 Jul 2009 08:49:03 +0200 |
krauss |
tuned
|
changeset |
files
|
| Tue, 28 Jul 2009 08:48:56 +0200 |
krauss |
moved obsolete same_fst to Recdef.thy
|
changeset |
files
|
| Tue, 28 Jul 2009 08:48:48 +0200 |
krauss |
adapted doc to type of "op O"
|
changeset |
files
|
| Tue, 28 Jul 2009 00:31:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jul 2009 23:43:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jul 2009 23:02:11 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jul 2009 22:25:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jul 2009 22:53:39 +0200 |
krauss |
added proof of Kleene_Algebra.star_decomp
|
changeset |
files
|
| Mon, 27 Jul 2009 22:50:04 +0200 |
krauss |
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
|
changeset |
files
|
| Mon, 27 Jul 2009 22:50:01 +0200 |
krauss |
some lemmas about maps (contributed by Peter Lammich)
|
changeset |
files
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
changeset |
files
|
| Tue, 28 Jul 2009 00:31:30 +0200 |
wenzelm |
added rail antiquotation environment, which coexists with old-style content markup;
|
changeset |
files
|
| Tue, 28 Jul 2009 00:27:58 +0200 |
wenzelm |
proper header;
|
changeset |
files
|
| Mon, 27 Jul 2009 23:17:40 +0200 |
wenzelm |
proper context for SAT tactics;
|
changeset |
files
|
| Mon, 27 Jul 2009 20:45:40 +0200 |
wenzelm |
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
|
changeset |
files
|
| Mon, 27 Jul 2009 17:36:30 +0200 |
wenzelm |
interruptible: Thread.testInterrupt before changing thread attributes;
|
changeset |
files
|
| Mon, 27 Jul 2009 17:12:19 +0200 |
wenzelm |
wait: absorb spurious interrupts;
|
changeset |
files
|
| Mon, 27 Jul 2009 16:53:28 +0200 |
wenzelm |
scheduler: shutdown spontaneously (after some delay) if queue is empty;
|
changeset |
files
|
| Mon, 27 Jul 2009 16:08:41 +0200 |
wenzelm |
join_next: do not yield, even if overloaded, to minimize "running" tasks;
|
changeset |
files
|
| Mon, 27 Jul 2009 15:53:43 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Mon, 27 Jul 2009 15:30:21 +0200 |
wenzelm |
cancel: improved reactivity due to more careful broadcasting;
|
changeset |
files
|
| Mon, 27 Jul 2009 15:06:33 +0200 |
wenzelm |
dequeue_towards: always return active tasks;
|
changeset |
files
|
| Mon, 27 Jul 2009 13:32:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jul 2009 13:32:23 +0200 |
wenzelm |
removed unused low-level interrupts;
|
changeset |
files
|
| Mon, 27 Jul 2009 12:24:27 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 27 Jul 2009 12:16:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 27 Jul 2009 12:11:18 +0200 |
wenzelm |
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
|
changeset |
files
|
| Mon, 27 Jul 2009 12:00:02 +0200 |
wenzelm |
enqueue/finish: return minimal/maximal state of this task;
|
changeset |
files
|
| Mon, 27 Jul 2009 09:01:13 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Sun, 26 Jul 2009 22:33:32 +0200 |
wenzelm |
tacticals FOCUS and FOCUS_PARAMS;
|
changeset |
files
|
| Sun, 26 Jul 2009 22:28:31 +0200 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
changeset |
files
|
| Sun, 26 Jul 2009 22:24:13 +0200 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
changeset |
files
|
| Sun, 26 Jul 2009 20:57:19 +0200 |
wenzelm |
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
|
changeset |
files
|
| Sun, 26 Jul 2009 20:38:11 +0200 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
changeset |
files
|
| Sun, 26 Jul 2009 19:54:37 +0200 |
wenzelm |
tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
|
changeset |
files
|
| Sun, 26 Jul 2009 19:38:02 +0200 |
wenzelm |
retrofit: actually handle schematic variables -- need to export into original context;
|
changeset |
files
|
| Sun, 26 Jul 2009 18:58:02 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 26 Jul 2009 08:03:40 +0200 |
haftmann |
adapted to changed prefixes
|
changeset |
files
|
| Sun, 26 Jul 2009 07:54:28 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 25 Jul 2009 18:44:55 +0200 |
haftmann |
improved handling of parameter import; tuned
|
changeset |
files
|
| Sat, 25 Jul 2009 18:44:55 +0200 |
haftmann |
explicit is better than implicit
|
changeset |
files
|
| Sat, 25 Jul 2009 18:44:54 +0200 |
haftmann |
localized interpretation of min/max-lattice
|
changeset |
files
|
| Sat, 25 Jul 2009 18:44:54 +0200 |
haftmann |
adapted to localized interpretation of min/max-lattice
|
changeset |
files
|
| Sun, 26 Jul 2009 18:57:11 +0200 |
wenzelm |
SUBPROOF/Obtain.result: named params;
|
changeset |
files
|
| Sun, 26 Jul 2009 13:21:12 +0200 |
wenzelm |
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
|
changeset |
files
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
advanced retrofit, which allows new subgoals and variables;
|
changeset |
files
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
Variable.focus: named parameters;
|
changeset |
files
|
| Sun, 26 Jul 2009 13:12:53 +0200 |
wenzelm |
lambda/cabs/all: named variants;
|
changeset |
files
|
| Sun, 26 Jul 2009 13:12:52 +0200 |
wenzelm |
Goal.finish: explicit context for printing;
|
changeset |
files
|
| Sat, 25 Jul 2009 18:55:30 +0200 |
wenzelm |
fixed Method.Basic;
|
changeset |
files
|
| Sat, 25 Jul 2009 18:55:12 +0200 |
wenzelm |
eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;
|
changeset |
files
|
| Sat, 25 Jul 2009 18:04:15 +0200 |
wenzelm |
Method.Basic: no position;
|
changeset |
files
|
| Sat, 25 Jul 2009 18:02:43 +0200 |
wenzelm |
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
|
changeset |
files
|
| Sat, 25 Jul 2009 14:58:45 +0200 |
wenzelm |
dequeue_towards: need to try imm_preds as well;
|
changeset |
files
|
| Sat, 25 Jul 2009 14:32:35 +0200 |
wenzelm |
internal session timing;
|
changeset |
files
|
| Sat, 25 Jul 2009 14:18:26 +0200 |
wenzelm |
enqueue: maintain transitive closure, which simplifies dequeue_towards;
|
changeset |
files
|
| Sat, 25 Jul 2009 13:15:53 +0200 |
wenzelm |
ML_Context.the_generic_context;
|
changeset |
files
|
| Sat, 25 Jul 2009 12:43:45 +0200 |
wenzelm |
eliminated redundant Library.multiply;
|
changeset |
files
|
| Sat, 25 Jul 2009 10:31:27 +0200 |
wenzelm |
renamed structure Display_Goal to Goal_Display;
|
changeset |
files
|
| Sat, 25 Jul 2009 00:53:47 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Sat, 25 Jul 2009 00:39:05 +0200 |
wenzelm |
added Multithreading.real_time;
|
changeset |
files
|
| Sat, 25 Jul 2009 00:13:39 +0200 |
wenzelm |
simplified/unified Multithreading.tracing_time;
|
changeset |
files
|
| Fri, 24 Jul 2009 23:36:37 +0200 |
wenzelm |
get_name: cover only PThm, not PAxm;
|
changeset |
files
|
| Fri, 24 Jul 2009 22:59:28 +0200 |
wenzelm |
eliminated OldGoals.read_term;
|
changeset |
files
|
| Fri, 24 Jul 2009 22:59:08 +0200 |
wenzelm |
more antiquotations instead of adhoc ML stuff;
|
changeset |
files
|
| Fri, 24 Jul 2009 22:31:27 +0200 |
wenzelm |
ML_Context.the_local_context;
|
changeset |
files
|
| Fri, 24 Jul 2009 22:17:32 +0200 |
wenzelm |
eliminated the_context;
|
changeset |
files
|
| Fri, 24 Jul 2009 22:09:09 +0200 |
wenzelm |
do not open OldGoals;
|
changeset |
files
|
| Fri, 24 Jul 2009 21:34:37 +0200 |
wenzelm |
renamed functor SplitterFun to Splitter, require explicit theory;
|
changeset |
files
|
| Fri, 24 Jul 2009 21:21:45 +0200 |
wenzelm |
renamed functor BlastFun to Blast, require explicit theory;
|
changeset |
files
|
| Fri, 24 Jul 2009 21:18:05 +0200 |
wenzelm |
eliminated OldGoals.prove_goal;
|
changeset |
files
|
| Fri, 24 Jul 2009 21:02:34 +0200 |
wenzelm |
explicit OldGoals;
|
changeset |
files
|
| Fri, 24 Jul 2009 20:55:56 +0200 |
wenzelm |
structure OldGoals: no pervasive names;
|
changeset |
files
|
| Fri, 24 Jul 2009 18:58:58 +0200 |
wenzelm |
renamed functor ProjectRuleFun to Project_Rule;
|
changeset |
files
|
| Fri, 24 Jul 2009 12:33:00 +0200 |
wenzelm |
renamed functor InductFun to Induct;
|
changeset |
files
|
| Fri, 24 Jul 2009 12:32:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 24 Jul 2009 12:00:02 +0200 |
wenzelm |
renamed Pure/tctical.ML to Pure/tactical.ML;
|
changeset |
files
|
| Fri, 24 Jul 2009 11:55:34 +0200 |
wenzelm |
eliminated print_goals_without_context -- proper pretty printing;
|
changeset |
files
|
| Fri, 24 Jul 2009 11:50:35 +0200 |
wenzelm |
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
|
changeset |
files
|
| Fri, 24 Jul 2009 11:31:22 +0200 |
wenzelm |
removed Formal_Power_Series_Examples (cf. adea7a729c7a);
|
changeset |
files
|
| Fri, 24 Jul 2009 11:30:32 +0200 |
wenzelm |
make: keep going by default;
|
changeset |
files
|
| Thu, 23 Jul 2009 23:43:45 +0200 |
chaieb |
merged
|
changeset |
files
|
| Thu, 23 Jul 2009 23:15:45 +0200 |
chaieb |
merged
|
changeset |
files
|
| Thu, 23 Jul 2009 22:25:09 +0200 |
chaieb |
fixed proof --- fact_setprod removed for fact_altdef_nat
|
changeset |
files
|
| Thu, 23 Jul 2009 21:13:21 +0200 |
chaieb |
merged
|
changeset |
files
|
| Thu, 23 Jul 2009 21:12:57 +0200 |
chaieb |
Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
|
changeset |
files
|
| Thu, 23 Jul 2009 21:12:57 +0200 |
chaieb |
More theorems about pochhammer
|
changeset |
files
|
| Wed, 15 Jul 2009 16:31:44 +0200 |
chaieb |
Moved theorem binomial_symmetric from Formal_Power_Series to here
|
changeset |
files
|
| Wed, 15 Jul 2009 06:14:25 +0200 |
chaieb |
Moved important theorems from FPS_Examples to FPS --- they are not
|
changeset |
files
|
| Thu, 23 Jul 2009 23:13:37 +0200 |
wenzelm |
removed obsolete ML proof tools;
|
changeset |
files
|
| Thu, 23 Jul 2009 23:12:21 +0200 |
wenzelm |
more @{theory} antiquotations;
|
changeset |
files
|
| Thu, 23 Jul 2009 22:20:37 +0200 |
wenzelm |
eliminated adhoc ML code;
|
changeset |
files
|
| Thu, 23 Jul 2009 21:59:56 +0200 |
wenzelm |
misc modernization: proper method setup instead of adhoc ML proofs;
|
changeset |
files
|
| Thu, 23 Jul 2009 20:05:20 +0200 |
wenzelm |
global_claset_of;
|
changeset |
files
|
| Thu, 23 Jul 2009 18:44:10 +0200 |
wenzelm |
Proper context for simpset_of, claset_of, clasimpset_of.
|
changeset |
files
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
local simpset_of;
|
changeset |
files
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
changeset |
files
|
| Thu, 23 Jul 2009 18:44:08 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
changeset |
files
|
| Thu, 23 Jul 2009 16:53:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 23 Jul 2009 16:53:00 +0200 |
wenzelm |
paramify_vars: Term_Subst.map_atypsT_same
|
changeset |
files
|
| Thu, 23 Jul 2009 16:52:16 +0200 |
wenzelm |
clarified pretty_goals, pretty_thm_aux: plain context;
|
changeset |
files
|
| Thu, 23 Jul 2009 16:43:31 +0200 |
wenzelm |
use regular Display.string_of_thm_global;
|
changeset |
files
|
| Thu, 23 Jul 2009 16:09:50 +0200 |
wenzelm |
tuned ML_OPTIONS;
|
changeset |
files
|
| Thu, 23 Jul 2009 15:59:14 +0200 |
haftmann |
fixed doc
|
changeset |
files
|
| Thu, 23 Jul 2009 09:38:22 +0200 |
berghofe |
Purely functional type inference.
|
changeset |
files
|
| Wed, 22 Jul 2009 18:08:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 22 Jul 2009 18:02:10 +0200 |
haftmann |
moved complete_lattice &c. into separate theory
|
changeset |
files
|
| Wed, 22 Jul 2009 15:28:49 +0200 |
Christian Urban |
merged
|
changeset |
files
|
| Wed, 22 Jul 2009 15:28:18 +0200 |
Christian Urban |
tuned proofs and added some lemmas
|
changeset |
files
|
| Wed, 22 Jul 2009 14:21:52 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 22 Jul 2009 14:20:32 +0200 |
haftmann |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
changeset |
files
|
| Wed, 22 Jul 2009 14:20:32 +0200 |
haftmann |
set intersection and union now named inter and union
|
changeset |
files
|
| Wed, 22 Jul 2009 14:20:31 +0200 |
haftmann |
spurious proof failure
|
changeset |
files
|
| Wed, 22 Jul 2009 11:48:04 +0200 |
wenzelm |
original rail implementation by Michael Kerscher;
|
changeset |
files
|
| Wed, 22 Jul 2009 11:23:09 +0200 |
wenzelm |
merged, resolving trivial conflict;
|
changeset |
files
|
| Wed, 22 Jul 2009 10:49:26 +0200 |
nipkow |
News
|
changeset |
files
|
| Wed, 22 Jul 2009 08:05:33 +0200 |
haftmann |
explicit antiquotation
|
changeset |
files
|
| Tue, 21 Jul 2009 17:03:40 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Jul 2009 17:02:18 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Jul 2009 16:14:56 +0200 |
haftmann |
obey captialized directory names convention
|
changeset |
files
|
| Tue, 21 Jul 2009 16:14:51 +0200 |
haftmann |
dropped ancient flat_names option
|
changeset |
files
|
| Tue, 21 Jul 2009 15:52:30 +0200 |
haftmann |
dropped ancient flat_names option
|
changeset |
files
|
| Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
integrated add_triv_classes into evaluation stack
|
changeset |
files
|
| Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
more accurate check of judgment type
|
changeset |
files
|
| Tue, 21 Jul 2009 15:44:30 +0200 |
haftmann |
UNIV_code now named UNIV_apply
|
changeset |
files
|
| Tue, 21 Jul 2009 14:38:07 +0200 |
haftmann |
attempt for more concise setup of non-etacontracting binders
|
changeset |
files
|
| Tue, 21 Jul 2009 14:36:26 +0200 |
haftmann |
moved abstract algebra section to the end
|
changeset |
files
|
| Tue, 21 Jul 2009 11:13:47 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Jul 2009 11:09:50 +0200 |
haftmann |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
changeset |
files
|
| Tue, 21 Jul 2009 07:55:56 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Jul 2009 07:54:44 +0200 |
haftmann |
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
|
changeset |
files
|
| Mon, 20 Jul 2009 16:50:59 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 20 Jul 2009 16:49:05 +0200 |
haftmann |
dropped add_registration interface in locale
|
changeset |
files
|
| Tue, 21 Jul 2009 14:08:58 +0200 |
nipkow |
Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
|
changeset |
files
|
| Tue, 21 Jul 2009 11:01:07 +0200 |
nipkow |
Tests for executability of "prime"
|
changeset |
files
|
| Wed, 22 Jul 2009 10:48:25 +0200 |
wenzelm |
less ambitious settings;
|
changeset |
files
|
| Wed, 22 Jul 2009 10:46:35 +0200 |
wenzelm |
future_job: more robust Exn.capture outside thread attribute change;
|
changeset |
files
|
| Wed, 22 Jul 2009 10:45:35 +0200 |
wenzelm |
shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
|
changeset |
files
|
| Tue, 21 Jul 2009 23:42:29 +0200 |
wenzelm |
future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
|
changeset |
files
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
maintain Future.worker_group as management data;
|
changeset |
files
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
join_proofs: implicit exception;
|
changeset |
files
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
simultaneous join_proofs;
|
changeset |
files
|