Tue, 25 May 1999 20:22:41 +0200 |
wenzelm |
renamed Comment.empty to Comment.none;
|
changeset |
files
|
Tue, 25 May 1999 20:21:30 +0200 |
wenzelm |
renamed Comment.empty to Comment.none;
|
changeset |
files
|
Tue, 25 May 1999 20:21:05 +0200 |
wenzelm |
renamed empty to none;
|
changeset |
files
|
Tue, 25 May 1999 20:19:59 +0200 |
wenzelm |
fixed cvs Id;
|
changeset |
files
|
Mon, 24 May 1999 21:57:13 +0200 |
wenzelm |
outer syntax keyword classification;
|
changeset |
files
|
Mon, 24 May 1999 21:56:14 +0200 |
wenzelm |
added keyword classification;
|
changeset |
files
|
Mon, 24 May 1999 21:55:34 +0200 |
wenzelm |
tuned print_context;
|
changeset |
files
|
Mon, 24 May 1999 21:54:34 +0200 |
wenzelm |
write_keywords generates outer syntax keyword classification in elisp;
|
changeset |
files
|
Mon, 24 May 1999 21:53:18 +0200 |
wenzelm |
outer syntax keyword classification;
|
changeset |
files
|
Mon, 24 May 1999 15:56:24 +0200 |
paulson |
renamed Lprg to Lift; simplified proof of Always_nonneg
|
changeset |
files
|
Mon, 24 May 1999 15:54:58 +0200 |
paulson |
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
|
changeset |
files
|
Mon, 24 May 1999 15:54:12 +0200 |
paulson |
Better simplification of (nat #0), (int (Suc 0)), etc
|
changeset |
files
|
Mon, 24 May 1999 15:53:28 +0200 |
paulson |
UN_singleton->UN_constant_eq removes clash with other UN_singleton
|
changeset |
files
|
Mon, 24 May 1999 15:51:33 +0200 |
paulson |
new rule single_leadsTo_I; stronger PSP rule
|
changeset |
files
|
Mon, 24 May 1999 15:50:53 +0200 |
paulson |
increasing makes sense only for partial orderings
|
changeset |
files
|
Mon, 24 May 1999 15:50:23 +0200 |
paulson |
generalized increasing_size to mono_increasing_o
|
changeset |
files
|
Mon, 24 May 1999 15:49:44 +0200 |
paulson |
updated for stronger version of psp
|
changeset |
files
|
Mon, 24 May 1999 15:49:24 +0200 |
paulson |
new rule single_LeadsTo_I; stronger PSP rule; PSP_stable2->PSP_Stable2
|
changeset |
files
|
Mon, 24 May 1999 15:48:27 +0200 |
paulson |
expandshort
|
changeset |
files
|
Mon, 24 May 1999 15:47:57 +0200 |
paulson |
lists are partially ordered by the prefix relation
|
changeset |
files
|
Mon, 24 May 1999 15:47:36 +0200 |
paulson |
using generic rules when possible
|
changeset |
files
|
Mon, 24 May 1999 15:47:06 +0200 |
paulson |
Theory of the "Follows" relation
|
changeset |
files
|
Mon, 24 May 1999 15:46:20 +0200 |
paulson |
Increasing makes sense only for partial orderings
|
changeset |
files
|
Mon, 24 May 1999 15:45:54 +0200 |
paulson |
generalized Increasing_size to mono_Increasing_o
|
changeset |
files
|
Mon, 24 May 1999 15:45:22 +0200 |
paulson |
tidied
|
changeset |
files
|
Mon, 24 May 1999 15:44:56 +0200 |
paulson |
renamed PSP_stable2->PSP_Stable2
|
changeset |
files
|
Mon, 24 May 1999 15:44:20 +0200 |
paulson |
now uses mono_Increasing_o
|
changeset |
files
|
Mon, 24 May 1999 15:43:45 +0200 |
paulson |
updated for stronger version of psp
|
changeset |
files
|
Fri, 21 May 1999 16:26:06 +0200 |
wenzelm |
Configuration for ProofGeneral of LFCS Edinburgh.
|
changeset |
files
|
Fri, 21 May 1999 16:25:49 +0200 |
wenzelm |
Configuration for David Aspinall's Isamode.
|
changeset |
files
|
Fri, 21 May 1999 16:25:34 +0200 |
wenzelm |
Miscellaneous interfaces.
|
changeset |
files
|
Fri, 21 May 1999 16:24:46 +0200 |
wenzelm |
Isamode.setup, ProofGeneral.setup;
|
changeset |
files
|
Fri, 21 May 1999 16:24:25 +0200 |
wenzelm |
Isamode and ProofGeneral configuration moved to Pure/Interface;
|
changeset |
files
|
Fri, 21 May 1999 16:23:48 +0200 |
wenzelm |
added use_thy_only;
|
changeset |
files
|
Fri, 21 May 1999 16:23:18 +0200 |
wenzelm |
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
|
changeset |
files
|
Fri, 21 May 1999 16:22:39 +0200 |
wenzelm |
avoid string constants;
|
changeset |
files
|
Fri, 21 May 1999 12:11:13 +0200 |
nipkow |
qed indexed.
|
changeset |
files
|
Fri, 21 May 1999 11:48:42 +0200 |
wenzelm |
typedef_proof: pass interactive flag;
|
changeset |
files
|
Fri, 21 May 1999 11:46:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 21 May 1999 11:43:34 +0200 |
wenzelm |
cleaned comments;
|
changeset |
files
|
Fri, 21 May 1999 11:41:46 +0200 |
wenzelm |
renamed 'begin' / 'end' to '{{' / '}}';
|
changeset |
files
|
Fri, 21 May 1999 11:40:34 +0200 |
wenzelm |
history commands;
|
changeset |
files
|
Fri, 21 May 1999 11:40:15 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 21 May 1999 11:39:47 +0200 |
wenzelm |
adapted to History changes;
|
changeset |
files
|
Fri, 21 May 1999 11:38:57 +0200 |
wenzelm |
local_qed: obtain interactive flag;
|
changeset |
files
|
Fri, 21 May 1999 11:38:23 +0200 |
wenzelm |
backup replaced by checkpoint;
|
changeset |
files
|
Fri, 21 May 1999 11:37:36 +0200 |
wenzelm |
added default_prompt;
|
changeset |
files
|
Fri, 21 May 1999 11:36:56 +0200 |
wenzelm |
optional limit;
|
changeset |
files
|
Fri, 21 May 1999 11:36:02 +0200 |
wenzelm |
improved errors;
|
changeset |
files
|
Fri, 21 May 1999 10:59:41 +0200 |
paulson |
updated comment
|
changeset |
files
|
Fri, 21 May 1999 10:58:47 +0200 |
paulson |
made definition more readable
|
changeset |
files
|
Fri, 21 May 1999 10:56:46 +0200 |
paulson |
preferring generic rules to specific ones...
|
changeset |
files
|
Fri, 21 May 1999 10:50:04 +0200 |
paulson |
changes to show that Lists are partially ordered by the prefix relation
|
changeset |
files
|
Fri, 21 May 1999 10:47:07 +0200 |
paulson |
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
|
changeset |
files
|
Wed, 19 May 1999 11:22:02 +0200 |
paulson |
redid proofs to use "always" rather than "reachable" (somewhat)
|
changeset |
files
|
Wed, 19 May 1999 11:21:34 +0200 |
paulson |
new theorem Always_reachable
|
changeset |
files
|
Tue, 18 May 1999 15:52:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 18 May 1999 12:36:06 +0200 |
paulson |
added Locale paper
|
changeset |
files
|
Tue, 18 May 1999 12:35:10 +0200 |
paulson |
locale documentation (from Florian)
|
changeset |
files
|
Tue, 18 May 1999 12:34:42 +0200 |
paulson |
../manual.bib a new dependency
|
changeset |
files
|
Mon, 17 May 1999 21:36:34 +0200 |
wenzelm |
cleaned comments;
|
changeset |
files
|
Mon, 17 May 1999 21:36:11 +0200 |
wenzelm |
cleaned comments;
|
changeset |
files
|
Mon, 17 May 1999 21:35:18 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 17 May 1999 21:34:45 +0200 |
wenzelm |
cleaned comments;
|
changeset |
files
|
Mon, 17 May 1999 21:33:22 +0200 |
wenzelm |
ThyInfo.finalize_all renamed to ThyInfo.finish;
|
changeset |
files
|
Mon, 17 May 1999 21:32:51 +0200 |
wenzelm |
node_cases renamed to node_case;
|
changeset |
files
|
Mon, 17 May 1999 21:32:08 +0200 |
wenzelm |
prep_ext exported (again);
|
changeset |
files
|
Mon, 17 May 1999 21:31:47 +0200 |
wenzelm |
backup operation replaces transaction;
|
changeset |
files
|
Mon, 17 May 1999 21:31:08 +0200 |
wenzelm |
removed get_nodes;
|
changeset |
files
|
Mon, 17 May 1999 19:15:35 +0200 |
wenzelm |
remove_thy;
|
changeset |
files
|
Mon, 17 May 1999 18:00:59 +0200 |
wenzelm |
tuned arrows;
|
changeset |
files
|
Mon, 17 May 1999 17:20:26 +0200 |
berghofe |
Arrows are no longer needed because of redesign of the
|
changeset |
files
|
Mon, 17 May 1999 17:18:31 +0200 |
berghofe |
Changed some file names.
|
changeset |
files
|
Mon, 17 May 1999 17:07:54 +0200 |
berghofe |
Added function get_preds.
|
changeset |
files
|
Mon, 17 May 1999 17:06:50 +0200 |
berghofe |
Added setup for BrowserInfo.
|
changeset |
files
|
Mon, 17 May 1999 17:04:26 +0200 |
berghofe |
usedir now recognizes additional option -P which is used to
|
changeset |
files
|
Mon, 17 May 1999 16:59:49 +0200 |
berghofe |
Changed interface of function use_dir.
|
changeset |
files
|
Mon, 17 May 1999 16:58:34 +0200 |
berghofe |
Present.begin_theory now needs an additional argument of type
|
changeset |
files
|
Mon, 17 May 1999 16:55:27 +0200 |
berghofe |
Reimplemented graph generator.
|
changeset |
files
|
Mon, 17 May 1999 16:48:58 +0200 |
berghofe |
Added some code to enable browser to display remote documents.
|
changeset |
files
|
Mon, 17 May 1999 10:38:47 +0200 |
paulson |
new thm extend_JN; renamed extend_leadsto
|
changeset |
files
|
Mon, 17 May 1999 10:38:08 +0200 |
paulson |
"component" now an infix
|
changeset |
files
|
Mon, 17 May 1999 10:37:07 +0200 |
paulson |
indentation
|
changeset |
files
|
Sat, 15 May 1999 16:15:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 12 May 1999 17:58:03 +0200 |
wenzelm |
ad-hoc fix for bold indexes;
|
changeset |
files
|
Wed, 12 May 1999 17:26:56 +0200 |
wenzelm |
strip_quotes replaced by unenclose;
|
changeset |
files
|
Wed, 12 May 1999 16:54:31 +0200 |
wenzelm |
rearranged some modules;
|
changeset |
files
|
Wed, 12 May 1999 16:52:28 +0200 |
wenzelm |
rearranged order of modules;
|
changeset |
files
|
Wed, 12 May 1999 16:51:52 +0200 |
wenzelm |
Basic URLs.
|
changeset |
files
|
Wed, 12 May 1999 16:50:56 +0200 |
wenzelm |
added url.ML;
|
changeset |
files
|
Wed, 12 May 1999 11:01:01 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Wed, 12 May 1999 09:44:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 11 May 1999 18:18:37 +0200 |
wenzelm |
fixed msg;
|
changeset |
files
|
Tue, 11 May 1999 17:51:23 +0200 |
wenzelm |
moved scan.ML;
|
changeset |
files
|
Tue, 11 May 1999 10:33:26 +0200 |
paulson |
new comments, variable renaming, etc
|
changeset |
files
|
Tue, 11 May 1999 10:32:45 +0200 |
paulson |
tidied
|
changeset |
files
|
Tue, 11 May 1999 10:32:10 +0200 |
paulson |
changes for new manual.bib
|
changeset |
files
|
Mon, 10 May 1999 17:45:16 +0200 |
wenzelm |
make pdf;
|
changeset |
files
|
Mon, 10 May 1999 17:44:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 10 May 1999 17:43:55 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Mon, 10 May 1999 17:07:19 +0200 |
wenzelm |
cite HOLCF;
|
changeset |
files
|
Mon, 10 May 1999 17:02:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 10 May 1999 16:48:00 +0200 |
wenzelm |
axclass;
|
changeset |
files
|
Mon, 10 May 1999 16:47:53 +0200 |
wenzelm |
axclass;
|
changeset |
files
|
Mon, 10 May 1999 16:35:22 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Mon, 10 May 1999 15:35:03 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Mon, 10 May 1999 15:32:58 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Mon, 10 May 1999 15:26:30 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Mon, 10 May 1999 15:17:14 +0200 |
wenzelm |
fixed URLs;
|
changeset |
files
|
Mon, 10 May 1999 15:16:49 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Fri, 07 May 1999 17:50:43 +0200 |
wenzelm |
replaced png by pdf;
|
changeset |
files
|
Fri, 07 May 1999 17:49:32 +0200 |
wenzelm |
pdf pics;
|
changeset |
files
|
Fri, 07 May 1999 11:02:00 +0200 |
paulson |
tidied
|
changeset |
files
|
Fri, 07 May 1999 10:50:28 +0200 |
paulson |
tidied
|
changeset |
files
|
Fri, 07 May 1999 10:48:56 +0200 |
paulson |
new refererences for Inductive manual, but still incomplete
|
changeset |
files
|
Thu, 06 May 1999 19:04:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 06 May 1999 19:04:20 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Thu, 06 May 1999 18:48:46 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Thu, 06 May 1999 18:46:50 +0200 |
wenzelm |
pdf setup;
|
changeset |
files
|
Thu, 06 May 1999 15:34:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 06 May 1999 11:48:26 +0200 |
nipkow |
More refs.
|
changeset |
files
|
Thu, 06 May 1999 11:48:09 +0200 |
nipkow |
Refs.
|
changeset |
files
|
Thu, 06 May 1999 11:13:01 +0200 |
nipkow |
New title page.
|
changeset |
files
|
Wed, 05 May 1999 18:48:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 05 May 1999 18:48:02 +0200 |
wenzelm |
manual.bib;
|
changeset |
files
|
Wed, 05 May 1999 18:47:37 +0200 |
wenzelm |
no rail;
|
changeset |
files
|
Wed, 05 May 1999 18:41:31 +0200 |
wenzelm |
fixed FILES;
|
changeset |
files
|
Wed, 05 May 1999 18:35:41 +0200 |
wenzelm |
improved Makefile;
|
changeset |
files
|
Wed, 05 May 1999 18:26:10 +0200 |
wenzelm |
improved Makefile;
|
changeset |
files
|
Wed, 05 May 1999 18:24:57 +0200 |
wenzelm |
isabelle.eps;
|
changeset |
files
|
Wed, 05 May 1999 18:19:03 +0200 |
wenzelm |
improved Makefile;
|
changeset |
files
|
Wed, 05 May 1999 18:16:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 05 May 1999 18:13:56 +0200 |
wenzelm |
improved Makefile;
|
changeset |
files
|
Wed, 05 May 1999 18:08:01 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Wed, 05 May 1999 18:07:38 +0200 |
wenzelm |
Common part for Doc Makefiles;
|
changeset |
files
|
Wed, 05 May 1999 16:44:42 +0200 |
paulson |
Now uses manual.bib; some references updated
|
changeset |
files
|
Wed, 05 May 1999 14:31:31 +0200 |
wenzelm |
tuned rpm file names;
|
changeset |
files
|
Wed, 05 May 1999 14:31:17 +0200 |
wenzelm |
updated docs;
|
changeset |
files
|
Wed, 05 May 1999 09:44:48 +0200 |
nipkow |
Bibtex database for documentation.
|
changeset |
files
|
Wed, 05 May 1999 09:43:53 +0200 |
nipkow |
Bibtex stuff.
|
changeset |
files
|
Tue, 04 May 1999 19:08:58 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Tue, 04 May 1999 18:56:43 +0200 |
wenzelm |
HOL;
|
changeset |
files
|
Tue, 04 May 1999 18:55:43 +0200 |
wenzelm |
removed HOL.tex;
|
changeset |
files
|
Tue, 04 May 1999 18:27:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 04 May 1999 18:11:35 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Tue, 04 May 1999 18:05:34 +0200 |
wenzelm |
HOL part moved to 'logics-HOL' manual;
|
changeset |
files
|
Tue, 04 May 1999 18:04:45 +0200 |
wenzelm |
fixed;
|
changeset |
files
|
Tue, 04 May 1999 18:03:56 +0200 |
wenzelm |
used to be part of 'logics' manual;
|
changeset |
files
|
Tue, 04 May 1999 17:59:55 +0200 |
wenzelm |
isabelle_zf image;
|
changeset |
files
|
Tue, 04 May 1999 17:59:31 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Tue, 04 May 1999 16:49:24 +0200 |
nipkow |
Arithmetic.
|
changeset |
files
|
Tue, 04 May 1999 16:18:16 +0200 |
wenzelm |
add_recdef: removed names / attributes;
|
changeset |
files
|
Tue, 04 May 1999 13:47:28 +0200 |
paulson |
new definitions of Co and LeadsTo
|
changeset |
files
|
Tue, 04 May 1999 13:32:53 +0200 |
wenzelm |
transaction: Theory.copy;
|
changeset |
files
|
Tue, 04 May 1999 13:32:35 +0200 |
wenzelm |
hide prep_ext, merge_theories;
|
changeset |
files
|
Tue, 04 May 1999 11:31:29 +0200 |
wenzelm |
oops;
|
changeset |
files
|
Tue, 04 May 1999 11:27:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 04 May 1999 10:26:00 +0200 |
paulson |
Invariant -> Always and other tidying
|
changeset |
files
|
Mon, 03 May 1999 19:03:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 03 May 1999 18:35:48 +0200 |
wenzelm |
theory loader stuff updated and improved;
|
changeset |
files
|
Mon, 03 May 1999 14:43:52 +0200 |
wenzelm |
fixed reqs?
|
changeset |
files
|
Mon, 03 May 1999 11:19:08 +0200 |
paulson |
improved error handling
|
changeset |
files
|
Mon, 03 May 1999 11:18:44 +0200 |
paulson |
renamed state variables
|
changeset |
files
|
Mon, 03 May 1999 11:18:11 +0200 |
paulson |
tidied
|
changeset |
files
|
Mon, 03 May 1999 10:57:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 03 May 1999 10:51:44 +0200 |
wenzelm |
prefer /bin for ./configure;
|
changeset |
files
|
Mon, 03 May 1999 10:47:32 +0200 |
wenzelm |
try chown root:root;
|
changeset |
files
|
Sat, 01 May 1999 00:10:05 +0200 |
wenzelm |
renamed 'dummy' to 'dummy_pattern' (less dangerous);
|
changeset |
files
|
Fri, 30 Apr 1999 18:25:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 30 Apr 1999 18:13:55 +0200 |
wenzelm |
method = meth3 (again);
|
changeset |
files
|
Fri, 30 Apr 1999 18:10:35 +0200 |
wenzelm |
peoper defer_recdef interface;
|
changeset |
files
|
Fri, 30 Apr 1999 18:10:03 +0200 |
wenzelm |
theory data: copy;
|
changeset |
files
|
Fri, 30 Apr 1999 18:09:33 +0200 |
wenzelm |
separated recdef / defer_recdef;
|
changeset |
files
|
Fri, 30 Apr 1999 18:08:58 +0200 |
wenzelm |
tuned defer_recdef interfaces;
|
changeset |
files
|
Fri, 30 Apr 1999 18:07:19 +0200 |
wenzelm |
comment, interest;
|
changeset |
files
|
Fri, 30 Apr 1999 18:06:49 +0200 |
wenzelm |
Comment.text;
|
changeset |
files
|
Fri, 30 Apr 1999 18:06:35 +0200 |
wenzelm |
comment sections;
|
changeset |
files
|
Fri, 30 Apr 1999 18:05:55 +0200 |
wenzelm |
dummy patterns;
|
changeset |
files
|
Fri, 30 Apr 1999 18:04:42 +0200 |
wenzelm |
added Isar/comment.ML;
|
changeset |
files
|
Fri, 30 Apr 1999 18:02:16 +0200 |
wenzelm |
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
|
changeset |
files
|
Fri, 30 Apr 1999 18:01:55 +0200 |
wenzelm |
theory data: copy;
|
changeset |
files
|
Fri, 30 Apr 1999 18:01:11 +0200 |
wenzelm |
theory data: copy;
|
changeset |
files
|
Fri, 30 Apr 1999 17:59:36 +0200 |
wenzelm |
improved icons;
|
changeset |
files
|
Fri, 30 Apr 1999 17:46:14 +0200 |
wenzelm |
Isabelle icons;
|
changeset |
files
|
Fri, 30 Apr 1999 16:41:10 +0200 |
wenzelm |
patched sum_case;
|
changeset |
files
|
Thu, 29 Apr 1999 22:45:19 +0200 |
berghofe |
Obsolete because JDK 1.1.x contains a class ScrollPane
|
changeset |
files
|
Thu, 29 Apr 1999 22:42:38 +0200 |
berghofe |
Updated to JDK 1.1.x
|
changeset |
files
|
Thu, 29 Apr 1999 18:34:30 +0200 |
nipkow |
Proof mods due to eta contraction during rewriting.
|
changeset |
files
|
Thu, 29 Apr 1999 18:33:31 +0200 |
nipkow |
Eta contraction is now performed all the time during rewriting.
|
changeset |
files
|
Thu, 29 Apr 1999 15:35:40 +0200 |
wenzelm |
currently disabled;
|
changeset |
files
|
Thu, 29 Apr 1999 15:34:43 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
Thu, 29 Apr 1999 10:51:58 +0200 |
paulson |
made many specification operators infix
|
changeset |
files
|
Wed, 28 Apr 1999 13:36:31 +0200 |
paulson |
eliminated theory UNITY/Traces
|
changeset |
files
|
Tue, 27 Apr 1999 15:39:43 +0200 |
wenzelm |
improper simp methods;
|
changeset |
files
|
Tue, 27 Apr 1999 15:32:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 27 Apr 1999 15:14:44 +0200 |
wenzelm |
fold / unfold methods;
|
changeset |
files
|
Tue, 27 Apr 1999 15:14:22 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 27 Apr 1999 15:13:58 +0200 |
wenzelm |
no Toplevel.print for by, ., ..;
|
changeset |
files
|
Tue, 27 Apr 1999 15:13:35 +0200 |
wenzelm |
improved print_state;
|
changeset |
files
|
Tue, 27 Apr 1999 15:13:18 +0200 |
wenzelm |
verbose flag;
|
changeset |
files
|
Tue, 27 Apr 1999 15:12:34 +0200 |
wenzelm |
use_thy_only made pervasive;
|
changeset |
files
|
Tue, 27 Apr 1999 15:10:36 +0200 |
wenzelm |
added Isar_examples/NatSum.thy;
|
changeset |
files
|
Tue, 27 Apr 1999 13:05:52 +0200 |
nipkow |
Old stuff.
|
changeset |
files
|
Tue, 27 Apr 1999 10:52:25 +0200 |
wenzelm |
proper quiet_mode;
|
changeset |
files
|
Tue, 27 Apr 1999 10:51:16 +0200 |
wenzelm |
adapted add_inductive, add_record;
|
changeset |
files
|
Tue, 27 Apr 1999 10:50:50 +0200 |
wenzelm |
adapted add_inductive;
|
changeset |
files
|
Tue, 27 Apr 1999 10:50:31 +0200 |
wenzelm |
intrs attributes;
|
changeset |
files
|
Tue, 27 Apr 1999 10:50:08 +0200 |
wenzelm |
proper quiet_mode;
|
changeset |
files
|
Tue, 27 Apr 1999 10:49:52 +0200 |
wenzelm |
iff_add_global (from simpdata.ML);
|
changeset |
files
|
Tue, 27 Apr 1999 10:47:40 +0200 |
wenzelm |
support forward chaining;
|
changeset |
files
|
Tue, 27 Apr 1999 10:46:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 27 Apr 1999 10:45:20 +0200 |
wenzelm |
added Isar_examples/Cantor.ML;
|
changeset |
files
|
Tue, 27 Apr 1999 10:44:42 +0200 |
wenzelm |
hol_setup, simpdata_setup;
|
changeset |
files
|
Tue, 27 Apr 1999 10:44:17 +0200 |
wenzelm |
"iff" attribute;
|
changeset |
files
|
Tue, 27 Apr 1999 10:43:52 +0200 |
wenzelm |
hol_setup;
|
changeset |
files
|
Tue, 27 Apr 1999 10:42:55 +0200 |
wenzelm |
"!" made keyword;
|
changeset |
files
|
Tue, 27 Apr 1999 10:42:37 +0200 |
wenzelm |
opt_thm_name: name optional;
|
changeset |
files
|
Tue, 27 Apr 1999 10:42:08 +0200 |
wenzelm |
added oooo;
|
changeset |
files
|
Mon, 26 Apr 1999 13:25:49 +0200 |
paulson |
fixed a bug many years old in rule plusEC
|
changeset |
files
|
Mon, 26 Apr 1999 10:44:45 +0200 |
wenzelm |
tuned msgs;
|
changeset |
files
|
Fri, 23 Apr 1999 17:47:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 23 Apr 1999 17:34:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 23 Apr 1999 17:02:10 +0200 |
wenzelm |
elaborated;
|
changeset |
files
|
Fri, 23 Apr 1999 17:01:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 23 Apr 1999 17:01:36 +0200 |
wenzelm |
tuned antiquotations;
|
changeset |
files
|
Fri, 23 Apr 1999 16:38:22 +0200 |
wenzelm |
improved 'single' method;
|
changeset |
files
|
Fri, 23 Apr 1999 16:33:23 +0200 |
wenzelm |
added thus, hence;
|
changeset |
files
|
Fri, 23 Apr 1999 16:33:03 +0200 |
wenzelm |
added FINISHED, same_tac;
|
changeset |
files
|
Fri, 23 Apr 1999 16:31:12 +0200 |
wenzelm |
use /usr/share and /usr/bin;
|
changeset |
files
|
Fri, 23 Apr 1999 12:23:21 +0200 |
paulson |
Now for recdefs that omit the WF relation;
|
changeset |
files
|
Fri, 23 Apr 1999 12:22:30 +0200 |
paulson |
Now for recdefs that omit the WF relation
|
changeset |
files
|
Fri, 23 Apr 1999 12:20:22 +0200 |
paulson |
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
|
changeset |
files
|
Fri, 23 Apr 1999 11:51:38 +0200 |
wenzelm |
chgrp isabelle;
|
changeset |
files
|
Fri, 23 Apr 1999 11:50:35 +0200 |
wenzelm |
detailed proofs;
|
changeset |
files
|
Fri, 23 Apr 1999 11:50:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 23 Apr 1999 11:48:37 +0200 |
wenzelm |
oops;
|
changeset |
files
|
Thu, 22 Apr 1999 18:25:24 +0200 |
wenzelm |
fixed IO;
|
changeset |
files
|
Thu, 22 Apr 1999 18:25:07 +0200 |
wenzelm |
improved load paths;
|
changeset |
files
|
Thu, 22 Apr 1999 18:23:45 +0200 |
wenzelm |
single method: include not_elim, imp_elim;
|
changeset |
files
|
Thu, 22 Apr 1999 18:20:37 +0200 |
wenzelm |
more graceful handling of load paths;
|
changeset |
files
|