| Mon, 13 Aug 2007 18:10:24 +0200 |
wenzelm |
moved appl syntax to PureThy;
|
changeset |
files
|
| Mon, 13 Aug 2007 18:10:24 +0200 |
wenzelm |
Lexicon.tokenize: do not appen EndToken yet;
|
changeset |
files
|
| Mon, 13 Aug 2007 18:10:22 +0200 |
wenzelm |
Lexicon.tokenize: do not appen EndToken yet;
|
changeset |
files
|
| Mon, 13 Aug 2007 18:10:22 +0200 |
wenzelm |
Lexicon.read_indexname/nat/variable;
|
changeset |
files
|
| Mon, 13 Aug 2007 18:10:20 +0200 |
wenzelm |
moved appl syntax to PureThy;
|
changeset |
files
|
| Mon, 13 Aug 2007 18:10:19 +0200 |
wenzelm |
moved appl syntax to PureThy;
|
changeset |
files
|
| Mon, 13 Aug 2007 18:10:18 +0200 |
wenzelm |
SimpleSyntax.read_prop;
|
changeset |
files
|
| Mon, 13 Aug 2007 12:56:03 +0200 |
isatest |
added atbroy9
|
changeset |
files
|
| Mon, 13 Aug 2007 12:53:58 +0200 |
isatest |
multi-threading with poly 5.1 test
|
changeset |
files
|
| Mon, 13 Aug 2007 04:35:41 +0200 |
kleing |
new attribute [rotated]
|
changeset |
files
|
| Mon, 13 Aug 2007 00:23:43 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 13 Aug 2007 00:17:57 +0200 |
wenzelm |
Simple syntax for types and terms --- for bootstrapping Pure.
|
changeset |
files
|
| Mon, 13 Aug 2007 00:17:54 +0200 |
wenzelm |
added Syntax/simple_syntax.ML;
|
changeset |
files
|
| Sun, 12 Aug 2007 19:00:58 +0200 |
wenzelm |
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
|
changeset |
files
|
| Sun, 12 Aug 2007 18:53:05 +0200 |
wenzelm |
read_def_terms': restrict scope of disambiguation to individual term;
|
changeset |
files
|
| Sun, 12 Aug 2007 18:53:04 +0200 |
wenzelm |
stream source: non-critical, assuming exclusive ownership;
|
changeset |
files
|
| Sun, 12 Aug 2007 18:53:03 +0200 |
wenzelm |
added type constraints to resolve syntax ambiguities;
|
changeset |
files
|
| Sun, 12 Aug 2007 14:14:24 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sat, 11 Aug 2007 17:50:23 +0200 |
wenzelm |
schedule_tasks: alphabetical order for equivalent tasks;
|
changeset |
files
|
| Fri, 10 Aug 2007 22:31:19 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Fri, 10 Aug 2007 18:21:25 +0200 |
wenzelm |
tuned ML bindings;
|
changeset |
files
|
| Fri, 10 Aug 2007 17:10:09 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 10 Aug 2007 17:10:06 +0200 |
haftmann |
dropped code generator setup garbage
|
changeset |
files
|
| Fri, 10 Aug 2007 17:10:05 +0200 |
haftmann |
syntax fix
|
changeset |
files
|
| Fri, 10 Aug 2007 17:10:04 +0200 |
haftmann |
corrected code generator module names
|
changeset |
files
|
| Fri, 10 Aug 2007 17:10:03 +0200 |
haftmann |
new structure for code generator modules
|
changeset |
files
|
| Fri, 10 Aug 2007 17:10:02 +0200 |
haftmann |
code generator setup improved
|
changeset |
files
|
| Fri, 10 Aug 2007 17:05:26 +0200 |
haftmann |
adjusted
|
changeset |
files
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
changeset |
files
|
| Fri, 10 Aug 2007 17:04:24 +0200 |
haftmann |
ClassPackage renamed to Class
|
changeset |
files
|
| Fri, 10 Aug 2007 17:04:20 +0200 |
haftmann |
updated
|
changeset |
files
|
| Fri, 10 Aug 2007 15:28:11 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Fri, 10 Aug 2007 15:13:18 +0200 |
paulson |
removal of some refs
|
changeset |
files
|
| Fri, 10 Aug 2007 14:49:01 +0200 |
wenzelm |
(un)interruptible: pass-through original thread attributes;
|
changeset |
files
|
| Fri, 10 Aug 2007 11:02:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 10 Aug 2007 10:54:19 +0200 |
wenzelm |
HOL_USEDIR_OPTIONS: default to -M 1 (more robust);
|
changeset |
files
|
| Fri, 10 Aug 2007 10:41:57 +0200 |
wenzelm |
added jEdit mode spec;
|
changeset |
files
|
| Fri, 10 Aug 2007 00:20:39 +0200 |
wenzelm |
* Experimental support for multithreading, using Poly/ML 5.1;
|
changeset |
files
|
| Thu, 09 Aug 2007 23:53:51 +0200 |
wenzelm |
schedule: misc cleanup, more precise task model;
|
changeset |
files
|
| Thu, 09 Aug 2007 23:53:50 +0200 |
wenzelm |
schedule: more precise task model;
|
changeset |
files
|
| Thu, 09 Aug 2007 23:53:49 +0200 |
wenzelm |
schedule: more precise task model;
|
changeset |
files
|
| Thu, 09 Aug 2007 19:19:23 +0200 |
wenzelm |
fixed DESCRIPTION: single line;
|
changeset |
files
|
| Thu, 09 Aug 2007 19:00:31 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 09 Aug 2007 16:56:17 +0200 |
wenzelm |
adapted ThyLoad.check_thy;
|
changeset |
files
|
| Thu, 09 Aug 2007 15:57:26 +0200 |
haftmann |
dropped
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:57 +0200 |
haftmann |
explizit checking for pattern discipline
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:56 +0200 |
haftmann |
proper handling of empty datatypes
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:55 +0200 |
haftmann |
improved class target: now considers class intro rules
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:54 +0200 |
haftmann |
new access interface in defs.ML
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:53 +0200 |
haftmann |
adaptions for code generation
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:49 +0200 |
haftmann |
proper implementation of rational numbers
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:47 +0200 |
haftmann |
localized of_nat
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:45 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:42 +0200 |
haftmann |
re-eliminated Option.thy
|
changeset |
files
|
| Thu, 09 Aug 2007 15:52:38 +0200 |
haftmann |
updated
|
changeset |
files
|
| Thu, 09 Aug 2007 11:39:29 +0200 |
aspinall |
PGIP change: thyname is optional in opentheory, markup even in case of header parse failure
|
changeset |
files
|
| Thu, 09 Aug 2007 11:37:27 +0200 |
aspinall |
Typo in comment
|
changeset |
files
|
| Wed, 08 Aug 2007 23:07:50 +0200 |
wenzelm |
discontinued attached ML files;
|
changeset |
files
|
| Wed, 08 Aug 2007 23:07:48 +0200 |
wenzelm |
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
|
changeset |
files
|
| Wed, 08 Aug 2007 23:07:47 +0200 |
wenzelm |
load_thy: try_ml_file unconditionally;
|
changeset |
files
|
| Wed, 08 Aug 2007 23:07:46 +0200 |
wenzelm |
* Theory loader: old-style ML proof scripts are considered a legacy feature;
|
changeset |
files
|
| Wed, 08 Aug 2007 20:48:08 +0200 |
wenzelm |
check_deps: really do reload the master text if required;
|
changeset |
files
|
| Wed, 08 Aug 2007 20:03:17 +0200 |
aspinall |
Useful abbreviation of isatool commands used by Eclipse
|
changeset |
files
|
| Wed, 08 Aug 2007 16:40:20 +0200 |
wenzelm |
thread-safeness: when creating certified items, perform Theory.check_thy *last*;
|
changeset |
files
|
| Wed, 08 Aug 2007 14:00:09 +0200 |
paulson |
Code to undo the function ascii_of
|
changeset |
files
|
| Wed, 08 Aug 2007 13:59:46 +0200 |
paulson |
Fixing the code to undo the function ascii_of
|
changeset |
files
|
| Wed, 08 Aug 2007 13:14:31 +0200 |
paulson |
metis
|
changeset |
files
|
| Tue, 07 Aug 2007 23:24:10 +0200 |
wenzelm |
tuned ML setup;
|
changeset |
files
|
| Tue, 07 Aug 2007 20:43:36 +0200 |
wenzelm |
fixed imports from ../../Auth;
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:55 +0200 |
wenzelm |
turned Unify flags into configuration options (global only);
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:54 +0200 |
wenzelm |
usedir: added options -M -T for multithreading;
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:52 +0200 |
wenzelm |
removed 'declare' from tactic emulations;
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:51 +0200 |
wenzelm |
theory loader: removed obsolete update_thy (coincides with use_thy);
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:50 +0200 |
wenzelm |
theory loader: removed obsolete update_thy (coincides with use_thy);
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:49 +0200 |
wenzelm |
theory loader: added use_thys, removed obsolete update_thy;
|
changeset |
files
|
| Tue, 07 Aug 2007 20:19:48 +0200 |
wenzelm |
theory loader: added use_thys, removed obsolete update_thy;
|
changeset |
files
|
| Tue, 07 Aug 2007 17:01:35 +0200 |
krauss |
Issue a warning, when "function" encounters variables occuring in function position,
|
changeset |
files
|
| Tue, 07 Aug 2007 15:20:24 +0200 |
krauss |
more error handling
|
changeset |
files
|
| Tue, 07 Aug 2007 15:04:35 +0200 |
wenzelm |
added more instances;
|
changeset |
files
|
| Tue, 07 Aug 2007 14:49:58 +0200 |
krauss |
simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"
|
changeset |
files
|
| Tue, 07 Aug 2007 10:03:25 +0200 |
haftmann |
split off Option theory
|
changeset |
files
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
changeset |
files
|
| Tue, 07 Aug 2007 09:38:48 +0200 |
haftmann |
more robust simproces
|
changeset |
files
|
| Tue, 07 Aug 2007 09:38:47 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 07 Aug 2007 09:38:46 +0200 |
haftmann |
simplified proofs
|
changeset |
files
|
| Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
changeset |
files
|
| Tue, 07 Aug 2007 09:38:43 +0200 |
haftmann |
changed import order
|
changeset |
files
|
| Mon, 06 Aug 2007 19:59:07 +0200 |
wenzelm |
added more instances;
|
changeset |
files
|
| Mon, 06 Aug 2007 19:58:59 +0200 |
wenzelm |
ML-Systems/overloading_smlnj.ML;
|
changeset |
files
|
| Mon, 06 Aug 2007 19:35:43 +0200 |
wenzelm |
Overloading in SML/NJ.
|
changeset |
files
|
| Mon, 06 Aug 2007 16:08:01 +0200 |
berghofe |
Added renaming function to prevent correctness proof for realizer
|
changeset |
files
|
| Mon, 06 Aug 2007 16:05:25 +0200 |
berghofe |
No document for Pretty_Int theory.
|
changeset |
files
|
| Mon, 06 Aug 2007 11:45:39 +0200 |
haftmann |
nbe improved
|
changeset |
files
|
| Mon, 06 Aug 2007 11:45:19 +0200 |
haftmann |
removed
|
changeset |
files
|
| Fri, 03 Aug 2007 22:50:40 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Fri, 03 Aug 2007 22:35:40 +0200 |
wenzelm |
reactivated Nominal/Examples/Class.thy;
|
changeset |
files
|
| Fri, 03 Aug 2007 22:33:10 +0200 |
wenzelm |
replaced outdated flag by update_time (multithreading-safe presentation order);
|
changeset |
files
|
| Fri, 03 Aug 2007 22:33:09 +0200 |
wenzelm |
sort indexes according to symbolic update_time (multithreading-safe);
|
changeset |
files
|
| Fri, 03 Aug 2007 22:33:07 +0200 |
wenzelm |
use separate trace flag instead of Output.debug;
|
changeset |
files
|
| Fri, 03 Aug 2007 22:33:03 +0200 |
wenzelm |
named some CRITICAL sections;
|
changeset |
files
|
| Fri, 03 Aug 2007 20:19:41 +0200 |
wenzelm |
misc cleanup of ML bindings (for multihreading);
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:25 +0200 |
wenzelm |
added int type constraint to accomodate hacked SML/NJ (backported change in generated metis.ML);
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:24 +0200 |
wenzelm |
preparations for proper type int;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:23 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:22 +0200 |
wenzelm |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:21 +0200 |
wenzelm |
certify: no check_thy here;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:20 +0200 |
wenzelm |
improved check_thy: produce a checked theory_ref (thread-safe version);
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:19 +0200 |
wenzelm |
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:18 +0200 |
wenzelm |
added dependency on Tools/Metis/metis.ML;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:17 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 03 Aug 2007 16:28:15 +0200 |
wenzelm |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
changeset |
files
|
| Thu, 02 Aug 2007 23:18:13 +0200 |
wenzelm |
reset Logic.auto_rename;
|
changeset |
files
|
| Thu, 02 Aug 2007 22:43:47 +0200 |
wenzelm |
added int type constraints to accomodate hacked SML/NJ;
|
changeset |
files
|
| Thu, 02 Aug 2007 22:16:49 +0200 |
wenzelm |
added int type constraints to accomodate hacked SML/NJ;
|
changeset |
files
|
| Thu, 02 Aug 2007 21:45:07 +0200 |
wenzelm |
added int type constraints to accomodate hacked SML/NJ;
|
changeset |
files
|
| Thu, 02 Aug 2007 21:43:55 +0200 |
wenzelm |
made mk_int/dest_int pervasive;
|
changeset |
files
|
| Thu, 02 Aug 2007 18:13:42 +0200 |
ballarin |
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
|
changeset |
files
|
| Thu, 02 Aug 2007 17:31:10 +0200 |
berghofe |
Repaired term_of_char.
|
changeset |
files
|
| Thu, 02 Aug 2007 17:29:40 +0200 |
berghofe |
- Added cycle test to function mk_ind_def to avoid non-termination
|
changeset |
files
|
| Thu, 02 Aug 2007 16:12:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 02 Aug 2007 15:44:37 +0200 |
wenzelm |
converted Meson tests to proper theory;
|
changeset |
files
|
| Thu, 02 Aug 2007 12:06:29 +0200 |
wenzelm |
turned simp_depth_limit into configuration option;
|
changeset |
files
|
| Thu, 02 Aug 2007 12:06:28 +0200 |
wenzelm |
added name_of;
|
changeset |
files
|
| Thu, 02 Aug 2007 12:06:27 +0200 |
wenzelm |
turned simp_depth_limit into configuration option;
|
changeset |
files
|
| Wed, 01 Aug 2007 21:10:36 +0200 |
wenzelm |
tuned ML bindings (for multithreading);
|
changeset |
files
|
| Wed, 01 Aug 2007 20:25:16 +0200 |
wenzelm |
tuned ML bindings (for multithreading);
|
changeset |
files
|
| Wed, 01 Aug 2007 19:59:12 +0200 |
huffman |
fix looping when applied to standard subgoals
|
changeset |
files
|
| Wed, 01 Aug 2007 18:05:43 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 01 Aug 2007 17:03:28 +0200 |
wenzelm |
tracing: level;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:59:15 +0200 |
wenzelm |
multithreading trace: int;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:45 +0200 |
wenzelm |
added toplevel print command;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:43 +0200 |
wenzelm |
renamed 'print_options' to 'print_configs';
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:42 +0200 |
wenzelm |
renamed config_option.ML to config.ML;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:41 +0200 |
wenzelm |
renamed config_option.ML to config.ML;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:40 +0200 |
wenzelm |
simplified internal Config interface;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:39 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:55:37 +0200 |
wenzelm |
tuned config options: eliminated separate attribute "option";
|
changeset |
files
|
| Wed, 01 Aug 2007 16:50:16 +0200 |
wenzelm |
oops -- fixed syntax;
|
changeset |
files
|
| Wed, 01 Aug 2007 16:48:47 +0200 |
wenzelm |
"running": PROTECTED wakeup;
|
changeset |
files
|
| Tue, 31 Jul 2007 23:23:34 +0200 |
wenzelm |
proper path specifications;
|
changeset |
files
|
| Tue, 31 Jul 2007 23:23:28 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Tue, 31 Jul 2007 22:21:22 +0200 |
wenzelm |
setmp_noncritical print_mode;
|
changeset |
files
|
| Tue, 31 Jul 2007 22:21:20 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Tue, 31 Jul 2007 22:21:18 +0200 |
wenzelm |
removed obsolete HOL/Real/ROOT.ML;
|
changeset |
files
|
| Tue, 31 Jul 2007 21:19:24 +0200 |
wenzelm |
no_document: setmp_noncritical;
|
changeset |
files
|
| Tue, 31 Jul 2007 21:19:23 +0200 |
wenzelm |
with_charset: setmp_noncritical;
|
changeset |
files
|
| Tue, 31 Jul 2007 21:19:22 +0200 |
wenzelm |
added max-threads preference;
|
changeset |
files
|
| Tue, 31 Jul 2007 21:19:21 +0200 |
wenzelm |
replaced depth_limit ref by blast_depth_limit configuration option;
|
changeset |
files
|
| Tue, 31 Jul 2007 21:19:20 +0200 |
wenzelm |
replaced dtK ref by datatype_distinctness_limit configuration option;
|
changeset |
files
|
| Tue, 31 Jul 2007 21:19:18 +0200 |
wenzelm |
moved classical tools from theory IFOL to FOL;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:40:28 +0200 |
wenzelm |
register_thy: more sanity checks;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:40:26 +0200 |
wenzelm |
moved lin_arith stuff to Tools/lin_arith.ML;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:40:25 +0200 |
wenzelm |
proper context for cooper_tac within arith;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:40:24 +0200 |
wenzelm |
tuned LinArith setup;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:40:23 +0200 |
wenzelm |
HOL setup for linear arithmetic -- moved here from arith_data.ML;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:40:22 +0200 |
wenzelm |
added Tools/lin_arith.ML;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:38:33 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 31 Jul 2007 19:26:35 +0200 |
wenzelm |
tuned section "Style";
|
changeset |
files
|
| Tue, 31 Jul 2007 14:45:36 +0200 |
narboux |
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
|
changeset |
files
|
| Tue, 31 Jul 2007 14:18:24 +0200 |
ballarin |
Proper interpretation of total orders in lattices.
|
changeset |
files
|
| Tue, 31 Jul 2007 13:31:01 +0200 |
wenzelm |
* Configuration options;
|
changeset |
files
|
| Tue, 31 Jul 2007 13:30:35 +0200 |
wenzelm |
added configuration options;
|
changeset |
files
|
| Tue, 31 Jul 2007 13:30:27 +0200 |
wenzelm |
removed use/update_thy_only;
|
changeset |
files
|
| Tue, 31 Jul 2007 09:31:26 +0200 |
chaieb |
find_body goes under meta-quantifier ; tactic generalizes free variables;
|
changeset |
files
|
| Tue, 31 Jul 2007 09:31:23 +0200 |
chaieb |
Added dependency on langford files in Tools/Qelim
|
changeset |
files
|
| Tue, 31 Jul 2007 09:31:19 +0200 |
chaieb |
Tuned document
|
changeset |
files
|
| Tue, 31 Jul 2007 00:56:34 +0200 |
wenzelm |
added register_thy (replaces pretend_use_thy_only and really flag);
|
changeset |
files
|
| Tue, 31 Jul 2007 00:56:32 +0200 |
wenzelm |
ThyInfo.register_thy;
|
changeset |
files
|
| Tue, 31 Jul 2007 00:56:31 +0200 |
wenzelm |
turned fast_arith_split/neq_limit into configuration options;
|
changeset |
files
|
| Tue, 31 Jul 2007 00:56:31 +0200 |
wenzelm |
added global config options;
|
changeset |
files
|
| Tue, 31 Jul 2007 00:56:29 +0200 |
wenzelm |
arith method setup: proper context;
|
changeset |
files
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
changeset |
files
|
| Mon, 30 Jul 2007 19:46:15 +0200 |
wenzelm |
tuned ML declarations;
|
changeset |
files
|
| Mon, 30 Jul 2007 19:46:13 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Mon, 30 Jul 2007 19:22:27 +0200 |
wenzelm |
dequeue: wait loop while PROTECTED -- avoids race condition;
|
changeset |
files
|
| Mon, 30 Jul 2007 11:12:28 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Mon, 30 Jul 2007 10:39:12 +0200 |
urbanc |
updated some of the definitions and proofs
|
changeset |
files
|
| Sun, 29 Jul 2007 23:27:40 +0200 |
wenzelm |
tuned msgs;
|
changeset |
files
|
| Sun, 29 Jul 2007 22:42:02 +0200 |
wenzelm |
deps: keep thy source text, avoid reloading;
|
changeset |
files
|
| Sun, 29 Jul 2007 22:42:00 +0200 |
wenzelm |
adapted ThyLoad.deps_thy;
|
changeset |
files
|
| Sun, 29 Jul 2007 22:41:59 +0200 |
wenzelm |
more informative tracing;
|
changeset |
files
|
| Sun, 29 Jul 2007 22:41:58 +0200 |
wenzelm |
load_thy: avoid reloading of text;
|
changeset |
files
|
| Sun, 29 Jul 2007 22:41:55 +0200 |
wenzelm |
added of_list_limited (with limit argument);
|
changeset |
files
|
| Sun, 29 Jul 2007 19:46:04 +0200 |
wenzelm |
more informative tracing;
|
changeset |
files
|
| Sun, 29 Jul 2007 19:46:03 +0200 |
wenzelm |
explicit global state argument -- no longer CRITICAL;
|
changeset |
files
|
| Sun, 29 Jul 2007 19:46:02 +0200 |
wenzelm |
added option -T (multithreading trace mode);
|
changeset |
files
|
| Sun, 29 Jul 2007 17:28:57 +0200 |
wenzelm |
critical: improved diagostics;
|
changeset |
files
|
| Sun, 29 Jul 2007 17:28:56 +0200 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Sun, 29 Jul 2007 17:28:55 +0200 |
wenzelm |
NAMED_CRITICAL;
|
changeset |
files
|
| Sun, 29 Jul 2007 16:00:06 +0200 |
wenzelm |
removed obsolete Output.ML_errors/toplevel_errors;
|
changeset |
files
|
| Sun, 29 Jul 2007 16:00:05 +0200 |
wenzelm |
removed obsolete Output.ML_errors/toplevel_errors;
|
changeset |
files
|
| Sun, 29 Jul 2007 16:00:04 +0200 |
wenzelm |
added TOPLEVEL_ERROR (simplified version from output.ML);
|
changeset |
files
|
| Sun, 29 Jul 2007 16:00:03 +0200 |
wenzelm |
removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);
|
changeset |
files
|
| Sun, 29 Jul 2007 16:00:02 +0200 |
wenzelm |
added ML toplevel use commands: Toplevel.program;
|
changeset |
files
|
| Sun, 29 Jul 2007 16:00:00 +0200 |
wenzelm |
removed obsolete install_pp.ML (cf. pure_setup.ML);
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:07 +0200 |
wenzelm |
replaced program_defs_ref by proper context data (via attribute "program");
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:06 +0200 |
wenzelm |
renamed Drule.is_dummy_thm to Thm.is_dummy;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:05 +0200 |
wenzelm |
added list update;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:04 +0200 |
wenzelm |
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:03 +0200 |
wenzelm |
Named collections of theorems in canonical order.
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:02 +0200 |
wenzelm |
added Tools/named_thms.ML;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:01 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:30:00 +0200 |
wenzelm |
avoid ill-defined Simp_tac;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:59 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:58 +0200 |
wenzelm |
simplified ResAtpset via NamedThmsFun;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:57 +0200 |
wenzelm |
metis_tac: proper context (ProofContext.init it *not* sufficient);
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:56 +0200 |
wenzelm |
proper simproc_setup for "neq", "let_simp";
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:54 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:52 +0200 |
wenzelm |
replaced make_imp by rev_mp;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:51 +0200 |
wenzelm |
proper simproc_setup for "list_neq";
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:50 +0200 |
wenzelm |
removed obsolete Tools/res_atpset.ML;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:49 +0200 |
wenzelm |
simplified ResAtpset via NamedThmsFun;
|
changeset |
files
|
| Sun, 29 Jul 2007 14:29:48 +0200 |
wenzelm |
simplified "eval" setup via NamedThmsFun;
|
changeset |
files
|
| Sat, 28 Jul 2007 22:19:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Jul 2007 22:17:46 +0200 |
wenzelm |
* Isar: command 'declaration';
|
changeset |
files
|
| Sat, 28 Jul 2007 22:01:06 +0200 |
wenzelm |
type Morphism.declaration;
|
changeset |
files
|
| Sat, 28 Jul 2007 22:01:01 +0200 |
wenzelm |
attribute "option": proper naming within the theory
|
changeset |
files
|
| Sat, 28 Jul 2007 22:01:00 +0200 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Sat, 28 Jul 2007 22:00:59 +0200 |
wenzelm |
declaration: proper naming within the theory;
|
changeset |
files
|
| Sat, 28 Jul 2007 22:00:58 +0200 |
wenzelm |
use config_option.ML after sign.ML;
|
changeset |
files
|
| Sat, 28 Jul 2007 21:09:14 +0200 |
wenzelm |
commands 'declare', 'declaration';
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:31 +0200 |
wenzelm |
added :|-- (dependent projection);
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:30 +0200 |
wenzelm |
added attribute "simproc";
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:29 +0200 |
wenzelm |
setmp: NAMED_CRITICAL;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:27 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:26 +0200 |
wenzelm |
added get_cs/map_cs;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:22 +0200 |
wenzelm |
tuned ML/simproc declarations;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:20 +0200 |
wenzelm |
removed redundant simproc declarations;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:19 +0200 |
wenzelm |
simproc_setup fun_upd2;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:18 +0200 |
wenzelm |
added [[decl]] notation;
|
changeset |
files
|
| Sat, 28 Jul 2007 20:40:17 +0200 |
wenzelm |
added command 'simproc_setup', attribute "simproc";
|
changeset |
files
|
| Fri, 27 Jul 2007 22:19:49 +0200 |
wenzelm |
attribs: not cut (!!!);
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:23 +0200 |
wenzelm |
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:22 +0200 |
wenzelm |
get_thm etc.: map empty name to dummy_thm;
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:21 +0200 |
wenzelm |
chain/using: filter out dummy_thm;
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:20 +0200 |
wenzelm |
method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:19 +0200 |
wenzelm |
renamed Config to ConfigOption;
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:18 +0200 |
wenzelm |
renamed Config to ConfigOption;
|
changeset |
files
|
| Fri, 27 Jul 2007 21:55:17 +0200 |
wenzelm |
renamed config.ML to config_option.ML;
|
changeset |
files
|
| Fri, 27 Jul 2007 20:11:49 +0200 |
wenzelm |
Druke.dummy_thm;
|
changeset |
files
|
| Fri, 27 Jul 2007 20:11:48 +0200 |
wenzelm |
added dummy_thm, is_dummy_thm;
|
changeset |
files
|
| Fri, 27 Jul 2007 20:11:47 +0200 |
wenzelm |
map_value: dynamic type checking;
|
changeset |
files
|
| Fri, 27 Jul 2007 16:31:16 +0200 |
wenzelm |
attribute "option": more elaborate syntax (with value parsing);
|
changeset |
files
|
| Fri, 27 Jul 2007 16:31:15 +0200 |
wenzelm |
added terminator, named_attribute;
|
changeset |
files
|
| Fri, 27 Jul 2007 16:31:14 +0200 |
wenzelm |
exported datatype value;
|
changeset |
files
|
| Fri, 27 Jul 2007 16:04:26 +0200 |
chaieb |
no 'nat' is needed for Bound in reification
|
changeset |
files
|
| Fri, 27 Jul 2007 10:18:56 +0200 |
haftmann |
*** empty log message ***
|
changeset |
files
|
| Fri, 27 Jul 2007 10:09:44 +0200 |
haftmann |
added cases
|
changeset |
files
|
| Thu, 26 Jul 2007 21:51:37 +0200 |
chaieb |
Updated proofs;
|
changeset |
files
|
| Thu, 26 Jul 2007 21:49:55 +0200 |
chaieb |
Updated reification : CX discontinued for CN
|
changeset |
files
|
| Thu, 26 Jul 2007 21:49:53 +0200 |
chaieb |
Updated proofs; changed shadow syntax to improve (processing) time
|
changeset |
files
|
| Thu, 26 Jul 2007 21:49:51 +0200 |
chaieb |
removed redundant ilcm_dvd1 ilcm_dvd2 zvdd_abs1
|
changeset |
files
|
| Thu, 26 Jul 2007 21:48:01 +0200 |
nipkow |
fixed broken proof
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:54 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:53 +0200 |
wenzelm |
renamed CRITICAL' to NAMED_CRITICAL;
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:52 +0200 |
wenzelm |
renamed CRITICAL' to NAMED_CRITICAL;
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:51 +0200 |
wenzelm |
added command 'print_options';
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:50 +0200 |
wenzelm |
added attribute "option" for setting configuration options;
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:49 +0200 |
wenzelm |
Configuration options as values within the local context.
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:48 +0200 |
wenzelm |
added config.ML;
|
changeset |
files
|
| Wed, 25 Jul 2007 22:20:47 +0200 |
wenzelm |
NAMED_CRITICAL;
|
changeset |
files
|
| Wed, 25 Jul 2007 18:10:49 +0200 |
nipkow |
fixed broken proof
|
changeset |
files
|
| Wed, 25 Jul 2007 18:10:28 +0200 |
nipkow |
Added lemmas
|
changeset |
files
|
| Wed, 25 Jul 2007 17:05:50 +0200 |
wenzelm |
require_thy/schedule: improved task graph, actually observe dependencies on running tasks;
|
changeset |
files
|
| Wed, 25 Jul 2007 17:05:49 +0200 |
wenzelm |
added trace flag, official tracing operation;
|
changeset |
files
|
| Wed, 25 Jul 2007 17:05:48 +0200 |
wenzelm |
added structure Task;
|
changeset |
files
|
| Wed, 25 Jul 2007 17:05:47 +0200 |
wenzelm |
Secure.use_noncritical root;
|
changeset |
files
|
| Wed, 25 Jul 2007 17:05:45 +0200 |
wenzelm |
added use_noncritical;
|
changeset |
files
|
| Wed, 25 Jul 2007 10:19:01 +0200 |
ballarin |
tuned
|
changeset |
files
|
| Tue, 24 Jul 2007 23:55:28 +0200 |
wenzelm |
fixed proofs involving dvd;
|
changeset |
files
|
| Tue, 24 Jul 2007 22:59:53 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Tue, 24 Jul 2007 22:53:49 +0200 |
wenzelm |
require_thy: tuned tasks graph, removed visited;
|
changeset |
files
|
| Tue, 24 Jul 2007 22:53:48 +0200 |
wenzelm |
renamed number_of_threads to max_threads;
|
changeset |
files
|
| Tue, 24 Jul 2007 22:53:46 +0200 |
wenzelm |
added usedir option -M: max threads;
|
changeset |
files
|
| Tue, 24 Jul 2007 21:51:18 +0200 |
krauss |
renamed lemma "set_take_whileD" to "set_takeWhileD"
|
changeset |
files
|
| Tue, 24 Jul 2007 20:34:11 +0200 |
urbanc |
cleaned up the proofs a bit
|
changeset |
files
|
| Tue, 24 Jul 2007 19:58:53 +0200 |
nipkow |
Added cancel simprocs for dvd on nat and int
|
changeset |
files
|
| Tue, 24 Jul 2007 19:46:44 +0200 |
wenzelm |
renamed to multithreading_dummy.ML;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:39 +0200 |
wenzelm |
require_thy: explicit tasks graph;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:38 +0200 |
wenzelm |
moved exception capture/release to structure Exn;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:37 +0200 |
wenzelm |
ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:36 +0200 |
wenzelm |
added topological_order;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:35 +0200 |
wenzelm |
moved exception capture/release to structure Exn;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:33 +0200 |
wenzelm |
Runtime exceptions as values (from library.ML);
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:32 +0200 |
wenzelm |
Multithreading in Poly/ML (version 5.1).
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:31 +0200 |
wenzelm |
Compatibility file for ML systems without multithreading.
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:30 +0200 |
wenzelm |
renamed ML-Systems/no_multithreading.ML to ML-Systems/multithreading_dummy.ML;
|
changeset |
files
|
| Tue, 24 Jul 2007 19:44:29 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Tue, 24 Jul 2007 15:29:57 +0200 |
ballarin |
Interpretation of rings (as integers) maps defined operations to defined
|
changeset |
files
|
| Tue, 24 Jul 2007 15:21:54 +0200 |
haftmann |
updated
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:53 +0200 |
haftmann |
added compile_term interface
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:52 +0200 |
haftmann |
swapped class projection order
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:51 +0200 |
haftmann |
interpretation_in
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:50 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:49 +0200 |
haftmann |
renamed lcm_lowest to lcm_least
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:48 +0200 |
haftmann |
dropped axclass
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:47 +0200 |
haftmann |
using interpretation with derived concepts
|
changeset |
files
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
changeset |
files
|
| Mon, 23 Jul 2007 22:18:05 +0200 |
wenzelm |
added proper implementation of self_critical, CRITICAL;
|
changeset |
files
|
| Mon, 23 Jul 2007 22:18:03 +0200 |
wenzelm |
added multithreading, self_critical
|
changeset |
files
|
| Mon, 23 Jul 2007 22:18:01 +0200 |
wenzelm |
RAW: updated deps;
|
changeset |
files
|
| Mon, 23 Jul 2007 20:47:56 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Mon, 23 Jul 2007 20:47:55 +0200 |
wenzelm |
added compatibility wrapper for polyml-5.1;
|
changeset |
files
|
| Mon, 23 Jul 2007 19:45:49 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Mon, 23 Jul 2007 19:45:48 +0200 |
wenzelm |
avoid global reference warned'';
|
changeset |
files
|
| Mon, 23 Jul 2007 19:45:47 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Mon, 23 Jul 2007 19:45:46 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Mon, 23 Jul 2007 19:45:45 +0200 |
wenzelm |
depth flag: plain bool ref;
|
changeset |
files
|
| Mon, 23 Jul 2007 19:45:44 +0200 |
wenzelm |
eliminated transform_failure (to avoid critical section for main transactions);
|
changeset |
files
|
| Mon, 23 Jul 2007 16:45:04 +0200 |
wenzelm |
setmp_noncritical (assumes outermost control);
|
changeset |
files
|
| Mon, 23 Jul 2007 16:45:03 +0200 |
wenzelm |
PrintMode.with_modes;
|
changeset |
files
|
| Mon, 23 Jul 2007 16:45:02 +0200 |
wenzelm |
added with_modes, with_default;
|
changeset |
files
|
| Mon, 23 Jul 2007 16:45:01 +0200 |
wenzelm |
marked some CRITICAL sections;
|
changeset |
files
|
| Mon, 23 Jul 2007 16:45:00 +0200 |
wenzelm |
added setmp_noncritical;
|
changeset |
files
|
| Mon, 23 Jul 2007 16:44:59 +0200 |
wenzelm |
PrintMode.with_default;
|
changeset |
files
|
| Mon, 23 Jul 2007 15:16:35 +0200 |
haftmann |
added nbe implementation heading for dictionaries
|
changeset |
files
|
| Mon, 23 Jul 2007 15:04:56 +0200 |
berghofe |
Tuned.
|
changeset |
files
|
| Mon, 23 Jul 2007 14:39:21 +0200 |
berghofe |
Protected underscore in inductive_set.
|
changeset |
files
|
| Mon, 23 Jul 2007 14:36:37 +0200 |
berghofe |
Replaced "hand-made" LaTeX code in Protocol/protocol.tex by
|
changeset |
files
|
| Mon, 23 Jul 2007 14:34:27 +0200 |
berghofe |
Removed legacy ML files in Protocol case study.
|
changeset |
files
|
| Mon, 23 Jul 2007 14:31:34 +0200 |
berghofe |
LaTeX code is now generated directly from theory files.
|
changeset |
files
|
| Mon, 23 Jul 2007 14:30:53 +0200 |
berghofe |
Ported ML proof scripts to Isar.
|
changeset |
files
|
| Mon, 23 Jul 2007 14:06:14 +0200 |
wenzelm |
hide internal structures (again);
|
changeset |
files
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
changeset |
files
|
| Mon, 23 Jul 2007 14:06:11 +0200 |
wenzelm |
added compatibility file for ML systems without multithreading;
|
changeset |
files
|
| Mon, 23 Jul 2007 13:50:31 +0200 |
ballarin |
interpretation: unfolding of equations;
|
changeset |
files
|
| Mon, 23 Jul 2007 13:48:30 +0200 |
ballarin |
interpretation: equations are propositions not pairs of terms;
|
changeset |
files
|
| Mon, 23 Jul 2007 13:47:48 +0200 |
ballarin |
interpretation: unfolding of equations;
|
changeset |
files
|
| Mon, 23 Jul 2007 01:17:57 +0200 |
kleing |
increase default max heap size for poly to -H 500 (this is what isatest uses,
|
changeset |
files
|
| Sun, 22 Jul 2007 23:33:57 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Sun, 22 Jul 2007 23:23:39 +0200 |
wenzelm |
fixed document;
|
changeset |
files
|
| Sun, 22 Jul 2007 22:01:30 +0200 |
wenzelm |
turned ex/prop.ML, ex/quant.ML into proper theories;
|
changeset |
files
|
| Sun, 22 Jul 2007 21:20:58 +0200 |
wenzelm |
inform_file_processed: tuned msg, no state;
|
changeset |
files
|
| Sun, 22 Jul 2007 21:20:56 +0200 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Sun, 22 Jul 2007 21:20:56 +0200 |
wenzelm |
init_empty: invoke operation *after* safe_exit;
|
changeset |
files
|
| Sun, 22 Jul 2007 21:20:55 +0200 |
wenzelm |
added simultaneous use_thys;
|
changeset |
files
|
| Sun, 22 Jul 2007 21:20:54 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Sun, 22 Jul 2007 21:20:53 +0200 |
wenzelm |
blast_hyp_subst_tac: plain bool argument;
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:55 +0200 |
chaieb |
Context data for QE in DLO (Langford's algorithm)
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:54 +0200 |
chaieb |
Quantifier elimination for Dense linear orders after Langford
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:51 +0200 |
chaieb |
Tuned proof : dlo replaced by ferrack
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:50 +0200 |
chaieb |
tuned
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:48 +0200 |
chaieb |
Renamed attribute dlo into attribute ferrack
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:45 +0200 |
chaieb |
Added quantifier elimination in dense linear orders after Langford; locale dense_linear_order renamed to constr_dense_linear_order (since it requires the beween constant). locale dense_linear_order is now the classical definition of DLO. constr_dense_linear_order is an instance of dense_linear_order; Method dlo now applies the langford QE, odl Method dlo renamed to ferrack, since it ia a QE only in interpretations where between is interpreted in a manner to vanish after substitution.
|
changeset |
files
|
| Sun, 22 Jul 2007 17:53:42 +0200 |
chaieb |
Tunes Proof
|
changeset |
files
|
| Sun, 22 Jul 2007 13:53:52 +0200 |
wenzelm |
begin_theory: simplified interface, keep thy info empty until end_theory;
|
changeset |
files
|
| Sun, 22 Jul 2007 13:53:51 +0200 |
wenzelm |
clarified init/begin_theory: no longer depend on thy_info.ML;
|
changeset |
files
|
| Sun, 22 Jul 2007 13:53:49 +0200 |
wenzelm |
clarified Present.init;
|
changeset |
files
|
| Sun, 22 Jul 2007 13:53:47 +0200 |
wenzelm |
simplified ThyInfo.begin_theory;
|
changeset |
files
|
| Sun, 22 Jul 2007 13:53:46 +0200 |
wenzelm |
load present.ML earlier: no longer depend on thy_info.ML;
|
changeset |
files
|
| Sun, 22 Jul 2007 11:58:23 +0200 |
wenzelm |
chmod u+rw on all files;
|
changeset |
files
|
| Sat, 21 Jul 2007 23:25:00 +0200 |
wenzelm |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
changeset |
files
|
| Sat, 21 Jul 2007 17:40:40 +0200 |
wenzelm |
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
|
changeset |
files
|
| Sat, 21 Jul 2007 17:40:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 21 Jul 2007 09:14:16 +0200 |
haftmann |
dropped Nat legacy bindings
|
changeset |
files
|
| Fri, 20 Jul 2007 19:54:03 +0200 |
wenzelm |
check_file: fall back on Path.current;
|
changeset |
files
|
| Fri, 20 Jul 2007 19:13:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 20 Jul 2007 19:10:05 +0200 |
wenzelm |
* Theory loader: be more serious about observing the static theory header specifications;
|
changeset |
files
|
| Fri, 20 Jul 2007 19:09:11 +0200 |
wenzelm |
added ISABELLE_FILE_IDENT;
|
changeset |
files
|
| Fri, 20 Jul 2007 17:54:17 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
changeset |
files
|
| Fri, 20 Jul 2007 17:54:17 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
changeset |
files
|
| Fri, 20 Jul 2007 17:54:15 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
changeset |
files
|
| Fri, 20 Jul 2007 15:29:25 +0200 |
obua |
new functions cut_matrix', etc.
|
changeset |
files
|
| Fri, 20 Jul 2007 14:33:40 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
changeset |
files
|
| Fri, 20 Jul 2007 14:28:25 +0200 |
haftmann |
moved class ord from Orderings.thy to HOL.thy
|
changeset |
files
|
| Fri, 20 Jul 2007 14:28:05 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
changeset |
files
|
| Fri, 20 Jul 2007 14:28:01 +0200 |
haftmann |
split class abs from class minus
|
changeset |
files
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
changeset |
files
|
| Fri, 20 Jul 2007 00:01:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:49:05 +0200 |
wenzelm |
ThyHeader.read: Source.of_string_limited;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:49:04 +0200 |
wenzelm |
added of_string_limited (more efficient for partial scans);
|
changeset |
files
|
| Thu, 19 Jul 2007 23:49:02 +0200 |
wenzelm |
added rep_ident;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:49:00 +0200 |
wenzelm |
added pprint for Path.T, File.ident;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:59 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:58 +0200 |
wenzelm |
removed obsolete use/update_thy_only;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:56 +0200 |
wenzelm |
adapted ThyLoad.check_file etc.;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:55 +0200 |
wenzelm |
adapted ThyLoad.deps_thy
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:55 +0200 |
wenzelm |
adapted ThyHeader.read;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:54 +0200 |
wenzelm |
adapted ThyLoad.check_file;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:52 +0200 |
wenzelm |
moved deps_thy to ThyLoad (independent of outer syntax);
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:51 +0200 |
wenzelm |
removed obsolete use/update_thy_only;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:50 +0200 |
wenzelm |
use thy_header.ML earlier;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:48 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:45 +0200 |
wenzelm |
replaced info by ident (for full identification, potentially content-based);
|
changeset |
files
|
| Thu, 19 Jul 2007 23:18:43 +0200 |
wenzelm |
added undefined: 'a -> 'b;
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:46 +0200 |
haftmann |
support for SML builtin ints
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:45 +0200 |
haftmann |
adapted to new code generator framework
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:44 +0200 |
haftmann |
code lemma for contents
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:43 +0200 |
haftmann |
code lemma for of_int
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:42 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:38 +0200 |
haftmann |
added lemmas by Brian Huffman
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:37 +0200 |
haftmann |
moved set Nats to Nat.thy
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:36 +0200 |
haftmann |
added of_int_of_nat
|
changeset |
files
|
| Thu, 19 Jul 2007 21:47:34 +0200 |
haftmann |
updated
|
changeset |
files
|
| Thu, 19 Jul 2007 15:37:37 +0200 |
berghofe |
strong_ind_simproc now only rewrites arguments of inductive predicates.
|
changeset |
files
|
| Thu, 19 Jul 2007 15:35:36 +0200 |
berghofe |
updated
|
changeset |
files
|
| Thu, 19 Jul 2007 15:35:00 +0200 |
berghofe |
Refer to major premise of induction rule via "thm_style prem1".
|
changeset |
files
|
| Thu, 19 Jul 2007 15:33:27 +0200 |
berghofe |
Added named_thms antiquotation.
|
changeset |
files
|
| Thu, 19 Jul 2007 15:32:58 +0200 |
berghofe |
Replaced "hand-made" files by generated files in Inductive/document.
|
changeset |
files
|
| Thu, 19 Jul 2007 15:31:30 +0200 |
berghofe |
LaTeX code is now generated directly from theory files.
|
changeset |
files
|
| Thu, 19 Jul 2007 15:30:35 +0200 |
berghofe |
LaTeX code is now generated directly from Even and Advanced theories.
|
changeset |
files
|
| Thu, 19 Jul 2007 15:29:51 +0200 |
berghofe |
LaTeX code is now generated directly from theory file.
|
changeset |
files
|
| Wed, 18 Jul 2007 14:46:59 +0200 |
aspinall |
DEEPEN: Use priority message channel for interim messages (not warnings).
|
changeset |
files
|
| Wed, 18 Jul 2007 14:44:49 +0200 |
aspinall |
Direct priority and tracing channels properly.
|
changeset |
files
|
| Wed, 18 Jul 2007 11:43:06 +0200 |
paulson |
tidying using metis
|
changeset |
files
|
| Tue, 17 Jul 2007 22:51:27 +0200 |
wenzelm |
fileident --- produce file identification based;
|
changeset |
files
|
| Tue, 17 Jul 2007 22:51:13 +0200 |
wenzelm |
added ISABELLE_FILE_IDENT (command line for source file identification);
|
changeset |
files
|
| Tue, 17 Jul 2007 22:48:40 +0200 |
wenzelm |
adapted TextIO.inputLine;
|
changeset |
files
|
| Tue, 17 Jul 2007 22:48:39 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Tue, 17 Jul 2007 16:14:42 +0200 |
wenzelm |
avoid redundant variables in patterns (which made Alice vomit);
|
changeset |
files
|
| Tue, 17 Jul 2007 16:06:13 +0200 |
paulson |
Full sort information by default.
|
changeset |
files
|
| Tue, 17 Jul 2007 16:05:54 +0200 |
berghofe |
Added hypotheses.
|
changeset |
files
|
| Tue, 17 Jul 2007 16:05:34 +0200 |
berghofe |
Added clause for hypotheses to proof_of_xml function.
|
changeset |
files
|
| Tue, 17 Jul 2007 15:59:50 +0200 |
wenzelm |
use /usr/proj/polyml/polyml-5.1-test, which might be more stable;
|
changeset |
files
|
| Tue, 17 Jul 2007 14:38:00 +0200 |
krauss |
reverted fun->recdef, since there are problems with induction rule
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:47 +0200 |
wenzelm |
Pure theory setup.
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:39 +0200 |
wenzelm |
Generic print mode.
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:21 +0200 |
wenzelm |
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:20 +0200 |
wenzelm |
simplified loading of ML files -- no static forward references;
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:19 +0200 |
wenzelm |
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:18 +0200 |
wenzelm |
added General/print_mode.ML, pure_setup.ML;
|
changeset |
files
|
| Tue, 17 Jul 2007 13:19:17 +0200 |
wenzelm |
tuned specifications;
|
changeset |
files
|
| Mon, 16 Jul 2007 21:39:56 +0200 |
krauss |
use function package
|
changeset |
files
|
| Mon, 16 Jul 2007 21:26:35 +0200 |
krauss |
more proofs
|
changeset |
files
|
| Mon, 16 Jul 2007 21:22:43 +0200 |
krauss |
some interface cleanup
|
changeset |
files
|
| Mon, 16 Jul 2007 21:17:12 +0200 |
krauss |
added lemma binding: accpI = accp.accI
|
changeset |
files
|
| Mon, 16 Jul 2007 21:16:16 +0200 |
krauss |
updated
|
changeset |
files
|
| Mon, 16 Jul 2007 19:18:23 +0200 |
paulson |
tidied using sledgehammer
|
changeset |
files
|
| Mon, 16 Jul 2007 19:11:37 +0200 |
paulson |
tidied
|
changeset |
files
|
| Mon, 16 Jul 2007 17:29:34 +0200 |
paulson |
tidied using sledgehammer
|
changeset |
files
|
| Mon, 16 Jul 2007 17:13:37 +0200 |
paulson |
tidied using sledgehammer
|
changeset |
files
|
| Mon, 16 Jul 2007 09:29:05 +0200 |
haftmann |
clarified structure names
|
changeset |
files
|
| Mon, 16 Jul 2007 09:29:04 +0200 |
haftmann |
added function for case certificates
|
changeset |
files
|
| Mon, 16 Jul 2007 09:29:03 +0200 |
haftmann |
dropped outer ROOT structure for generated code
|
changeset |
files
|
| Mon, 16 Jul 2007 09:29:02 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 16 Jul 2007 09:29:01 +0200 |
haftmann |
fixed SML/NJ int problem
|
changeset |
files
|
| Mon, 16 Jul 2007 09:29:00 +0200 |
haftmann |
updated
|
changeset |
files
|
| Fri, 13 Jul 2007 22:36:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 12 Jul 2007 12:20:39 +0200 |
krauss |
updated
|
changeset |
files
|
| Thu, 12 Jul 2007 11:43:17 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:42 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:41 +0200 |
wenzelm |
sys_error;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:39 +0200 |
wenzelm |
simplified using Markup.get_int;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:38 +0200 |
wenzelm |
added skeleton for print_mode setup;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:37 +0200 |
wenzelm |
tuned spacing;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:36 +0200 |
wenzelm |
renamed PgipParser to OldPgipParser;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:35 +0200 |
wenzelm |
Parsing theory sources without execution (via keyword classification).
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:34 +0200 |
wenzelm |
exported command_keyword;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:30 +0200 |
wenzelm |
command 'declare': proper thy_decl;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:28 +0200 |
wenzelm |
added get_string, get_int;
|
changeset |
files
|
| Thu, 12 Jul 2007 00:15:26 +0200 |
wenzelm |
added ProofGeneral/pgip_parser.ML;
|
changeset |
files
|
| Wed, 11 Jul 2007 19:22:05 +0200 |
wenzelm |
tuned error faces;
|
changeset |
files
|
| Wed, 11 Jul 2007 18:25:30 +0200 |
nipkow |
tries to solve goal via TrueI
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:52 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:51 +0200 |
wenzelm |
replaced OuterLex.name_of by more sophisticated OuterLex.text_of;
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:50 +0200 |
wenzelm |
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:49 +0200 |
wenzelm |
Buffer.markup;
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:48 +0200 |
wenzelm |
removed ident, space;
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:47 +0200 |
wenzelm |
added markup operation;
|
changeset |
files
|
| Wed, 11 Jul 2007 17:47:45 +0200 |
wenzelm |
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
|
changeset |
files
|
| Wed, 11 Jul 2007 12:23:34 +0200 |
berghofe |
Added entry for new inductive definition package.
|
changeset |
files
|
| Wed, 11 Jul 2007 12:01:10 +0200 |
berghofe |
Proof terms for meta-conjunctions are now normalized before
|
changeset |
files
|
| Wed, 11 Jul 2007 11:59:21 +0200 |
berghofe |
Added function norm_proof for normalizing the proof term
|
changeset |
files
|
| Wed, 11 Jul 2007 11:58:40 +0200 |
berghofe |
Added function rew_proof (for pre-normalizing proofs).
|
changeset |
files
|
| Wed, 11 Jul 2007 11:56:59 +0200 |
berghofe |
Function unify_consts moved from OldInductivePackage to PrimrecPackage.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:54:21 +0200 |
berghofe |
Adapted to new inductive definition package.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:54:03 +0200 |
berghofe |
Renamed accessible part for predicates to accp.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:52:45 +0200 |
berghofe |
renamed inductive2 to inductive.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:52:28 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:52:00 +0200 |
berghofe |
Hide member constant.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:51:15 +0200 |
berghofe |
Reverted renaming of "member".
|
changeset |
files
|
| Wed, 11 Jul 2007 11:51:12 +0200 |
obua |
changed sources for HOL-Complex-Matrix
|
changeset |
files
|
| Wed, 11 Jul 2007 11:49:56 +0200 |
berghofe |
Restored set notation in Multiset theory.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:47:59 +0200 |
obua |
added dummy makestring function
|
changeset |
files
|
| Wed, 11 Jul 2007 11:47:24 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
changeset |
files
|
| Wed, 11 Jul 2007 11:47:13 +0200 |
obua |
fixed for SML/NJ
|
changeset |
files
|