wenzelm [Sat, 28 Jul 2007 22:17:46 +0200] rev 24032
* Isar: command 'declaration';
* Isar: proper interfaces for simplification procedures;
* Isar: an extra pair of brackets around attribute declarations
abbreviates a theorem reference involving an internal dummy fact;
wenzelm [Sat, 28 Jul 2007 22:01:06 +0200] rev 24031
type Morphism.declaration;
wenzelm [Sat, 28 Jul 2007 22:01:01 +0200] rev 24030
attribute "option": proper naming within the theory
wenzelm [Sat, 28 Jul 2007 22:01:00 +0200] rev 24029
removed dead code;
wenzelm [Sat, 28 Jul 2007 22:00:59 +0200] rev 24028
declaration: proper naming within the theory;
wenzelm [Sat, 28 Jul 2007 22:00:58 +0200] rev 24027
use config_option.ML after sign.ML;
wenzelm [Sat, 28 Jul 2007 21:09:14 +0200] rev 24026
commands 'declare', 'declaration';
wenzelm [Sat, 28 Jul 2007 20:40:31 +0200] rev 24025
added :|-- (dependent projection);
tuned;
wenzelm [Sat, 28 Jul 2007 20:40:30 +0200] rev 24024
added attribute "simproc";
marked some CRITICAL sections;
tuned;
wenzelm [Sat, 28 Jul 2007 20:40:29 +0200] rev 24023
setmp: NAMED_CRITICAL;
wenzelm [Sat, 28 Jul 2007 20:40:27 +0200] rev 24022
tuned;
wenzelm [Sat, 28 Jul 2007 20:40:26 +0200] rev 24021
added get_cs/map_cs;
wenzelm [Sat, 28 Jul 2007 20:40:24 +0200] rev 24020
tuned signature;
wenzelm [Sat, 28 Jul 2007 20:40:22 +0200] rev 24019
tuned ML/simproc declarations;
wenzelm [Sat, 28 Jul 2007 20:40:20 +0200] rev 24018
removed redundant simproc declarations;
wenzelm [Sat, 28 Jul 2007 20:40:19 +0200] rev 24017
simproc_setup fun_upd2;
wenzelm [Sat, 28 Jul 2007 20:40:18 +0200] rev 24016
added [[decl]] notation;
wenzelm [Sat, 28 Jul 2007 20:40:17 +0200] rev 24015
added command 'simproc_setup', attribute "simproc";
wenzelm [Fri, 27 Jul 2007 22:19:49 +0200] rev 24014
attribs: not cut (!!!);
wenzelm [Fri, 27 Jul 2007 21:55:23 +0200] rev 24013
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm [Fri, 27 Jul 2007 21:55:22 +0200] rev 24012
get_thm etc.: map empty name to dummy_thm;
wenzelm [Fri, 27 Jul 2007 21:55:21 +0200] rev 24011
chain/using: filter out dummy_thm;
wenzelm [Fri, 27 Jul 2007 21:55:20 +0200] rev 24010
method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;
wenzelm [Fri, 27 Jul 2007 21:55:19 +0200] rev 24009
renamed Config to ConfigOption;
wenzelm [Fri, 27 Jul 2007 21:55:18 +0200] rev 24008
renamed Config to ConfigOption;
thm scanners: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm [Fri, 27 Jul 2007 21:55:17 +0200] rev 24007
renamed config.ML to config_option.ML;
wenzelm [Fri, 27 Jul 2007 20:11:49 +0200] rev 24006
Druke.dummy_thm;
wenzelm [Fri, 27 Jul 2007 20:11:48 +0200] rev 24005
added dummy_thm, is_dummy_thm;
wenzelm [Fri, 27 Jul 2007 20:11:47 +0200] rev 24004
map_value: dynamic type checking;
wenzelm [Fri, 27 Jul 2007 16:31:16 +0200] rev 24003
attribute "option": more elaborate syntax (with value parsing);
wenzelm [Fri, 27 Jul 2007 16:31:15 +0200] rev 24002
added terminator, named_attribute;
wenzelm [Fri, 27 Jul 2007 16:31:14 +0200] rev 24001
exported datatype value;
added the_config;
removed put_generic_src -- moved value parsing to attrib.ML;
tuned;
chaieb [Fri, 27 Jul 2007 16:04:26 +0200] rev 24000
no 'nat' is needed for Bound in reification
haftmann [Fri, 27 Jul 2007 10:18:56 +0200] rev 23999
*** empty log message ***
haftmann [Fri, 27 Jul 2007 10:09:44 +0200] rev 23998
added cases
chaieb [Thu, 26 Jul 2007 21:51:37 +0200] rev 23997
Updated proofs;
chaieb [Thu, 26 Jul 2007 21:49:55 +0200] rev 23996
Updated reification : CX discontinued for CN
chaieb [Thu, 26 Jul 2007 21:49:53 +0200] rev 23995
Updated proofs; changed shadow syntax to improve (processing) time
chaieb [Thu, 26 Jul 2007 21:49:51 +0200] rev 23994
removed redundant ilcm_dvd1 ilcm_dvd2 zvdd_abs1
nipkow [Thu, 26 Jul 2007 21:48:01 +0200] rev 23993
fixed broken proof
wenzelm [Wed, 25 Jul 2007 22:20:54 +0200] rev 23992
updated;
wenzelm [Wed, 25 Jul 2007 22:20:53 +0200] rev 23991
renamed CRITICAL' to NAMED_CRITICAL;
tuned messages;
wenzelm [Wed, 25 Jul 2007 22:20:52 +0200] rev 23990
renamed CRITICAL' to NAMED_CRITICAL;
wenzelm [Wed, 25 Jul 2007 22:20:51 +0200] rev 23989
added command 'print_options';
wenzelm [Wed, 25 Jul 2007 22:20:50 +0200] rev 23988
added attribute "option" for setting configuration options;
wenzelm [Wed, 25 Jul 2007 22:20:49 +0200] rev 23987
Configuration options as values within the local context.
wenzelm [Wed, 25 Jul 2007 22:20:48 +0200] rev 23986
added config.ML;
wenzelm [Wed, 25 Jul 2007 22:20:47 +0200] rev 23985
NAMED_CRITICAL;
nipkow [Wed, 25 Jul 2007 18:10:49 +0200] rev 23984
fixed broken proof
nipkow [Wed, 25 Jul 2007 18:10:28 +0200] rev 23983
Added lemmas
wenzelm [Wed, 25 Jul 2007 17:05:50 +0200] rev 23982
require_thy/schedule: improved task graph, actually observe dependencies on running tasks;
wenzelm [Wed, 25 Jul 2007 17:05:49 +0200] rev 23981
added trace flag, official tracing operation;
added named CRITICAL';
schedule: tuned signature, actually observe dependencies on running tasks;
wenzelm [Wed, 25 Jul 2007 17:05:48 +0200] rev 23980
added structure Task;
added trace flag, official tracing operation;
added named CRITICAL';
schedule: tuned signature;
wenzelm [Wed, 25 Jul 2007 17:05:47 +0200] rev 23979
Secure.use_noncritical root;
wenzelm [Wed, 25 Jul 2007 17:05:45 +0200] rev 23978
added use_noncritical;
ballarin [Wed, 25 Jul 2007 10:19:01 +0200] rev 23977
tuned
wenzelm [Tue, 24 Jul 2007 23:55:28 +0200] rev 23976
fixed proofs involving dvd;
wenzelm [Tue, 24 Jul 2007 22:59:53 +0200] rev 23975
*** empty log message ***
wenzelm [Tue, 24 Jul 2007 22:53:49 +0200] rev 23974
require_thy: tuned tasks graph, removed visited;
use_thy etc.: schedule for multithreading;
wenzelm [Tue, 24 Jul 2007 22:53:48 +0200] rev 23973
renamed number_of_threads to max_threads;
added schedule operator;