Sun, 26 Mar 2000 20:08:03 +0200 |
wenzelm |
tuned targets;
|
changeset |
files
|
Sat, 25 Mar 2000 18:01:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 25 Mar 2000 17:59:52 +0100 |
wenzelm |
improved (anti)quote_tr(');
|
changeset |
files
|
Sat, 25 Mar 2000 13:00:44 +0100 |
wenzelm |
addsimprocs [record_simproc];
|
changeset |
files
|
Sat, 25 Mar 2000 12:59:31 +0100 |
wenzelm |
tuned antiquote_tr';
|
changeset |
files
|
Sat, 25 Mar 2000 12:52:06 +0100 |
wenzelm |
export updateN;
|
changeset |
files
|
Fri, 24 Mar 2000 21:15:56 +0100 |
wenzelm |
use abstract syntax;
|
changeset |
files
|
Fri, 24 Mar 2000 21:09:34 +0100 |
wenzelm |
plain ASCII;
|
changeset |
files
|
Fri, 24 Mar 2000 20:59:15 +0100 |
wenzelm |
arith method: HEADGOAL;
|
changeset |
files
|
Fri, 24 Mar 2000 17:29:51 +0100 |
wenzelm |
HOL/ex/Multiquote;
|
changeset |
files
|
Fri, 24 Mar 2000 17:28:03 +0100 |
wenzelm |
added HOL/ex/Multiquote.thy;
|
changeset |
files
|
Fri, 24 Mar 2000 14:40:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 24 Mar 2000 13:48:31 +0100 |
wenzelm |
usedir -D: update styles as well;
|
changeset |
files
|
Fri, 24 Mar 2000 13:48:01 +0100 |
wenzelm |
usedir -D: update styles;
|
changeset |
files
|
Fri, 24 Mar 2000 13:47:36 +0100 |
wenzelm |
improved dump of styles;
|
changeset |
files
|
Fri, 24 Mar 2000 11:52:19 +0100 |
wenzelm |
-o sty;
|
changeset |
files
|
Fri, 24 Mar 2000 08:56:48 +0100 |
nipkow |
comments
|
changeset |
files
|
Thu, 23 Mar 2000 21:37:13 +0100 |
wenzelm |
added 'moreover' command;
|
changeset |
files
|
Thu, 23 Mar 2000 21:36:43 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
Thu, 23 Mar 2000 11:28:10 +0100 |
wenzelm |
tuned spacing;
|
changeset |
files
|
Thu, 23 Mar 2000 11:27:52 +0100 |
wenzelm |
ex/Antiquote.thy made new-style theory;
|
changeset |
files
|
Thu, 23 Mar 2000 10:23:54 +0100 |
paulson |
now exclusively uses rtac/dtac/etac rather than the long forms
|
changeset |
files
|
Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
changeset |
files
|
Wed, 22 Mar 2000 13:23:57 +0100 |
paulson |
made a proof more robust (did not like Suc_less_eq)
|
changeset |
files
|
Wed, 22 Mar 2000 13:22:39 +0100 |
paulson |
Suc_less_eq now with AddIffs. How could this have been overlooked?
|
changeset |
files
|
Wed, 22 Mar 2000 13:22:11 +0100 |
paulson |
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
|
changeset |
files
|
Wed, 22 Mar 2000 13:01:57 +0100 |
paulson |
made more robust
|
changeset |
files
|
Wed, 22 Mar 2000 13:01:18 +0100 |
paulson |
tidied using new "inst" rule
|
changeset |
files
|
Wed, 22 Mar 2000 12:45:41 +0100 |
paulson |
tidied using new "inst" rule
|
changeset |
files
|
Wed, 22 Mar 2000 12:33:34 +0100 |
paulson |
new meta-rule "inst", a shorthand for read_instantiate_sg
|
changeset |
files
|