Thu, 04 Sep 2008 16:43:48 +0200 Efficient queues.
wenzelm [Thu, 04 Sep 2008 16:43:48 +0200] rev 28127
Efficient queues.
Thu, 04 Sep 2008 16:03:49 +0200 moved Multithreading.task/schedule to Concurrent/schedule.ML
wenzelm [Thu, 04 Sep 2008 16:03:49 +0200] rev 28126
moved Multithreading.task/schedule to Concurrent/schedule.ML
Thu, 04 Sep 2008 16:03:48 +0200 multithreading.ML provides dummy thread structures;
wenzelm [Thu, 04 Sep 2008 16:03:48 +0200] rev 28125
multithreading.ML provides dummy thread structures;
Thu, 04 Sep 2008 16:03:47 +0200 moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm [Thu, 04 Sep 2008 16:03:47 +0200] rev 28124
moved Multithreading.task/schedule to Concurrent/schedule.ML;
Thu, 04 Sep 2008 16:03:46 +0200 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm [Thu, 04 Sep 2008 16:03:46 +0200] rev 28123
provide dummy thread structures, including proper Thread.getLocal/setLocal; moved task/schedule to Concurrent/schedule.ML;
Thu, 04 Sep 2008 16:03:44 +0200 Thread.getLocal/setLocal;
wenzelm [Thu, 04 Sep 2008 16:03:44 +0200] rev 28122
Thread.getLocal/setLocal;
Thu, 04 Sep 2008 16:03:43 +0200 Scheduling -- multiple threads working on a queue of tasks.
wenzelm [Thu, 04 Sep 2008 16:03:43 +0200] rev 28121
Scheduling -- multiple threads working on a queue of tasks. formerly in ML-Systems/multithreading_polyml.ML; simplified -- less tracing; use regular Isabelle/ML functions instead of NJ stuff;
Thu, 04 Sep 2008 16:03:41 +0200 added Concurrent/schedule.ML;
wenzelm [Thu, 04 Sep 2008 16:03:41 +0200] rev 28120
added Concurrent/schedule.ML;
Wed, 03 Sep 2008 20:32:33 +0000 update tags
convert-repo [Wed, 03 Sep 2008 20:32:33 +0000] rev 28119
update tags
Wed, 03 Sep 2008 20:04:54 +0200 use /home/isabelle/mercurial/bin/hg wrapper;
wenzelm [Wed, 03 Sep 2008 20:04:54 +0200] rev 28118
use /home/isabelle/mercurial/bin/hg wrapper;
Wed, 03 Sep 2008 19:52:45 +0200 exclude large .mov files;
wenzelm [Wed, 03 Sep 2008 19:52:45 +0200] rev 28117
exclude large .mov files;
Wed, 03 Sep 2008 17:50:37 +0200 simplified add_axiom: no hyps;
wenzelm [Wed, 03 Sep 2008 17:50:37 +0200] rev 28116
simplified add_axiom: no hyps;
Wed, 03 Sep 2008 17:47:40 +0200 discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
wenzelm [Wed, 03 Sep 2008 17:47:40 +0200] rev 28115
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
Wed, 03 Sep 2008 17:47:38 +0200 axiomatization is now global-only;
wenzelm [Wed, 03 Sep 2008 17:47:38 +0200] rev 28114
axiomatization is now global-only;
Wed, 03 Sep 2008 17:47:37 +0200 added const_decl;
wenzelm [Wed, 03 Sep 2008 17:47:37 +0200] rev 28113
added const_decl;
Wed, 03 Sep 2008 17:47:35 +0200 simplified specify_const: canonical args, global deps;
wenzelm [Wed, 03 Sep 2008 17:47:35 +0200] rev 28112
simplified specify_const: canonical args, global deps;
Wed, 03 Sep 2008 17:47:34 +0200 declare_const: Name.binding, store/report position;
wenzelm [Wed, 03 Sep 2008 17:47:34 +0200] rev 28111
declare_const: Name.binding, store/report position;
Wed, 03 Sep 2008 17:47:30 +0200 Sign.declare_const: Name.binding;
wenzelm [Wed, 03 Sep 2008 17:47:30 +0200] rev 28110
Sign.declare_const: Name.binding;
Wed, 03 Sep 2008 12:11:28 +0200 removed ex/Puzzle
nipkow [Wed, 03 Sep 2008 12:11:28 +0200] rev 28109
removed ex/Puzzle
Wed, 03 Sep 2008 11:44:52 +0200 added qualified: string -> binding -> binding;
wenzelm [Wed, 03 Sep 2008 11:44:52 +0200] rev 28108
added qualified: string -> binding -> binding;
Wed, 03 Sep 2008 11:44:48 +0200 Name.qualified;
wenzelm [Wed, 03 Sep 2008 11:44:48 +0200] rev 28107
Name.qualified;
Wed, 03 Sep 2008 11:27:15 +0200 theorem dependency hook: check previous state;
wenzelm [Wed, 03 Sep 2008 11:27:15 +0200] rev 28106
theorem dependency hook: check previous state;
Wed, 03 Sep 2008 11:26:59 +0200 added pos_of;
wenzelm [Wed, 03 Sep 2008 11:26:59 +0200] rev 28105
added pos_of;
Wed, 03 Sep 2008 11:18:55 +0200 -> AFP
nipkow [Wed, 03 Sep 2008 11:18:55 +0200] rev 28104
-> AFP
Wed, 03 Sep 2008 11:09:08 +0200 simplified Toplevel.add_hook: cover successful transactions only;
wenzelm [Wed, 03 Sep 2008 11:09:08 +0200] rev 28103
simplified Toplevel.add_hook: cover successful transactions only;
Wed, 03 Sep 2008 00:11:27 +0200 retired Ben Porter's DenumRat in favour of the shorter proof in
kleing [Wed, 03 Sep 2008 00:11:27 +0200] rev 28102
retired Ben Porter's DenumRat in favour of the shorter proof in Real/Rational.thy
Tue, 02 Sep 2008 23:52:51 +0200 made SML/NJ happy;
wenzelm [Tue, 02 Sep 2008 23:52:51 +0200] rev 28101
made SML/NJ happy;
Tue, 02 Sep 2008 23:27:44 +0200 refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm [Tue, 02 Sep 2008 23:27:44 +0200] rev 28100
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel); new_thms_deps: explicity theory values;
Tue, 02 Sep 2008 22:41:36 +0200 * Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm [Tue, 02 Sep 2008 22:41:36 +0200] rev 28099
* Generic Toplevel.add_hook interface allows to analyze the result of transactions (including failed ones). For example, see src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency output of transactions resulting in a new theory state.
Tue, 02 Sep 2008 22:37:20 +0200 Replaced Library/NatPair by Nat_Int_Bij.
nipkow [Tue, 02 Sep 2008 22:37:20 +0200] rev 28098
Replaced Library/NatPair by Nat_Int_Bij.
Tue, 02 Sep 2008 22:20:27 +0200 added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm [Tue, 02 Sep 2008 22:20:27 +0200] rev 28097
added new_thms_deps (operates on global facts, some name_hint approximation); theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
Tue, 02 Sep 2008 22:20:25 +0200 theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
wenzelm [Tue, 02 Sep 2008 22:20:25 +0200] rev 28096
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
Tue, 02 Sep 2008 22:20:24 +0200 added add_hook interface for post-transition hooks;
wenzelm [Tue, 02 Sep 2008 22:20:24 +0200] rev 28095
added add_hook interface for post-transition hooks;
Tue, 02 Sep 2008 22:20:21 +0200 tuned;
wenzelm [Tue, 02 Sep 2008 22:20:21 +0200] rev 28094
tuned;
Tue, 02 Sep 2008 22:20:20 +0200 ProofDisplay.print_results;
wenzelm [Tue, 02 Sep 2008 22:20:20 +0200] rev 28093
ProofDisplay.print_results;
Tue, 02 Sep 2008 22:20:16 +0200 no pervasive bindings;
wenzelm [Tue, 02 Sep 2008 22:20:16 +0200] rev 28092
no pervasive bindings; removed theory_results and related hook; print_results: ignore empty/internal kind -- like former theory_results;
Tue, 02 Sep 2008 21:31:28 +0200 Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow [Tue, 02 Sep 2008 21:31:28 +0200] rev 28091
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.
Tue, 02 Sep 2008 20:38:17 +0200 distributed literal code generation out of central infrastructure
haftmann [Tue, 02 Sep 2008 20:38:17 +0200] rev 28090
distributed literal code generation out of central infrastructure
Tue, 02 Sep 2008 20:07:51 +0200 * Result facts now refer to the *full* internal name;
wenzelm [Tue, 02 Sep 2008 20:07:51 +0200] rev 28089
* Result facts now refer to the *full* internal name;
Tue, 02 Sep 2008 20:04:26 +0200 * Name bindings in higher specification mechanisms;
wenzelm [Tue, 02 Sep 2008 20:04:26 +0200] rev 28088
* Name bindings in higher specification mechanisms;
Tue, 02 Sep 2008 18:01:24 +0200 pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
wenzelm [Tue, 02 Sep 2008 18:01:24 +0200] rev 28087
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
Tue, 02 Sep 2008 18:01:23 +0200 updated generated file;
wenzelm [Tue, 02 Sep 2008 18:01:23 +0200] rev 28086
updated generated file;
Tue, 02 Sep 2008 17:31:20 +0200 Interpretation commands no longer accept interpretation attributes.
ballarin [Tue, 02 Sep 2008 17:31:20 +0200] rev 28085
Interpretation commands no longer accept interpretation attributes.
Tue, 02 Sep 2008 16:55:33 +0200 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm [Tue, 02 Sep 2008 16:55:33 +0200] rev 28084
type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
Tue, 02 Sep 2008 14:10:45 +0200 explicit type Name.binding for higher-specification elements;
wenzelm [Tue, 02 Sep 2008 14:10:45 +0200] rev 28083
explicit type Name.binding for higher-specification elements;
Tue, 02 Sep 2008 14:10:32 +0200 explicit type Name.binding for higher-specification elements;
wenzelm [Tue, 02 Sep 2008 14:10:32 +0200] rev 28082
explicit type Name.binding for higher-specification elements; report local_fact_decl, fixed_decl; simplified ProofContext.inferred_param;
Tue, 02 Sep 2008 14:10:31 +0200 explicit type Name.binding for higher-specification elements;
wenzelm [Tue, 02 Sep 2008 14:10:31 +0200] rev 28081
explicit type Name.binding for higher-specification elements; added binding, parbinding;
Tue, 02 Sep 2008 14:10:30 +0200 explicit type Name.binding for higher-specification elements;
wenzelm [Tue, 02 Sep 2008 14:10:30 +0200] rev 28080
explicit type Name.binding for higher-specification elements; simplified ProofContext.inferred_param;
Tue, 02 Sep 2008 14:10:29 +0200 explicit type Name.binding for higher-specification elements;
wenzelm [Tue, 02 Sep 2008 14:10:29 +0200] rev 28079
explicit type Name.binding for higher-specification elements; name/var morphism operates on Name.binding;
Tue, 02 Sep 2008 14:10:28 +0200 added binding;
wenzelm [Tue, 02 Sep 2008 14:10:28 +0200] rev 28078
added binding; thm_name/opt_thm_name: Name.binding;
Tue, 02 Sep 2008 14:10:27 +0200 added fixed_decl, fact_decl, local_fact_decl;
wenzelm [Tue, 02 Sep 2008 14:10:27 +0200] rev 28077
added fixed_decl, fact_decl, local_fact_decl;
Tue, 02 Sep 2008 14:10:25 +0200 name_thm etc.: pass position;
wenzelm [Tue, 02 Sep 2008 14:10:25 +0200] rev 28076
name_thm etc.: pass position; note_thms etc.: Name.binding, report fact_decl;
Tue, 02 Sep 2008 14:10:24 +0200 added type binding -- generic name bindings;
wenzelm [Tue, 02 Sep 2008 14:10:24 +0200] rev 28075
added type binding -- generic name bindings;
Tue, 02 Sep 2008 14:10:19 +0200 name/var morphism operates on Name.binding;
wenzelm [Tue, 02 Sep 2008 14:10:19 +0200] rev 28074
name/var morphism operates on Name.binding;
Tue, 02 Sep 2008 12:07:34 +0200 adapted to class instantiation compliance
haftmann [Tue, 02 Sep 2008 12:07:34 +0200] rev 28073
adapted to class instantiation compliance
Mon, 01 Sep 2008 22:10:42 +0200 It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
nipkow [Mon, 01 Sep 2008 22:10:42 +0200] rev 28072
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
Mon, 01 Sep 2008 19:17:47 +0200 renamed lemma
nipkow [Mon, 01 Sep 2008 19:17:47 +0200] rev 28071
renamed lemma
Mon, 01 Sep 2008 19:17:37 +0200 moved more lemmas here from AFP/Integration/Rats
nipkow [Mon, 01 Sep 2008 19:17:37 +0200] rev 28070
moved more lemmas here from AFP/Integration/Rats
Mon, 01 Sep 2008 19:17:04 +0200 moved lemma into SetInterval where it belongs
nipkow [Mon, 01 Sep 2008 19:17:04 +0200] rev 28069
moved lemma into SetInterval where it belongs
Mon, 01 Sep 2008 19:16:40 +0200 cleaned up code generation for {.._} and {..<_}
nipkow [Mon, 01 Sep 2008 19:16:40 +0200] rev 28068
cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong
Mon, 01 Sep 2008 10:28:04 +0200 *** empty log message ***
nipkow [Mon, 01 Sep 2008 10:28:04 +0200] rev 28067
*** empty log message ***
Mon, 01 Sep 2008 10:20:14 +0200 extended interface to preferences to allow adding new ones
nipkow [Mon, 01 Sep 2008 10:20:14 +0200] rev 28066
extended interface to preferences to allow adding new ones
Mon, 01 Sep 2008 10:19:38 +0200 Prover is set via menu now
nipkow [Mon, 01 Sep 2008 10:19:38 +0200] rev 28065
Prover is set via menu now
Mon, 01 Sep 2008 10:18:37 +0200 restructured code generation of literals
haftmann [Mon, 01 Sep 2008 10:18:37 +0200] rev 28064
restructured code generation of literals
(0) -10000 -3000 -1000 -300 -100 -64 +64 +100 +300 +1000 +3000 +10000 +30000 tip