Tue, 28 Oct 1997 17:36:16 +0100 |
wenzelm |
added ignored_consts, thms_containing, add_store_axioms(_i),
|
changeset |
files
|
Tue, 28 Oct 1997 17:34:12 +0100 |
wenzelm |
always reload .ML *and* .thy file;
|
changeset |
files
|
Tue, 28 Oct 1997 17:32:38 +0100 |
wenzelm |
PureThy.add_store_defs, PureThy.add_store_axioms;
|
changeset |
files
|
Tue, 28 Oct 1997 17:31:55 +0100 |
wenzelm |
added ancestors;
|
changeset |
files
|
Tue, 28 Oct 1997 17:30:47 +0100 |
wenzelm |
added name_of_thm;
|
changeset |
files
|
Tue, 28 Oct 1997 17:29:48 +0100 |
wenzelm |
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
|
changeset |
files
|
Tue, 28 Oct 1997 17:28:11 +0100 |
wenzelm |
eq_thm moved to thm.ML;
|
changeset |
files
|
Tue, 28 Oct 1997 17:27:10 +0100 |
wenzelm |
add_store_axioms_i;
|
changeset |
files
|
Tue, 28 Oct 1997 14:03:25 +0100 |
nipkow |
Added finite_UNION/SigmaI.
|
changeset |
files
|
Mon, 27 Oct 1997 16:01:53 +0100 |
wenzelm |
oops;
|
changeset |
files
|
Mon, 27 Oct 1997 15:57:50 +0100 |
wenzelm |
renamed put_* to store_*;
|
changeset |
files
|
Mon, 27 Oct 1997 15:43:53 +0100 |
wenzelm |
flipped global_names default;
|
changeset |
files
|
Mon, 27 Oct 1997 15:43:16 +0100 |
wenzelm |
do not change global_names flag;
|
changeset |
files
|
Mon, 27 Oct 1997 15:29:01 +0100 |
wenzelm |
Isa94-2 instead of Isa95;
|
changeset |
files
|
Mon, 27 Oct 1997 11:34:33 +0100 |
oheimb |
adapted domain and ax_ops package for name spaces
|
changeset |
files
|
Mon, 27 Oct 1997 10:46:36 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
Mon, 27 Oct 1997 10:34:17 +0100 |
paulson |
Deleted two needless theorems
|
changeset |
files
|
Sat, 25 Oct 1997 14:43:55 +0200 |
oheimb |
internalized some names
|
changeset |
files
|
Sat, 25 Oct 1997 14:39:25 +0200 |
oheimb |
corrected two comments
|
changeset |
files
|
Fri, 24 Oct 1997 18:10:51 +0200 |
nipkow |
Added
|
changeset |
files
|
Fri, 24 Oct 1997 18:02:23 +0200 |
wenzelm |
oops, swap warnings;
|
changeset |
files
|
Fri, 24 Oct 1997 17:28:20 +0200 |
wenzelm |
record: tuned output;
|
changeset |
files
|
Fri, 24 Oct 1997 17:25:33 +0200 |
wenzelm |
ProtoPure.flexpair_def;
|
changeset |
files
|
Fri, 24 Oct 1997 17:19:14 +0200 |
wenzelm |
ProtoPure.flexpair_def;
|
changeset |
files
|
Fri, 24 Oct 1997 17:18:49 +0200 |
wenzelm |
merge: default to ProtoPure.thy;
|
changeset |
files
|
Fri, 24 Oct 1997 17:18:25 +0200 |
wenzelm |
ProtoPure.thy etc.;
|
changeset |
files
|
Fri, 24 Oct 1997 17:18:00 +0200 |
wenzelm |
tuned names;
|
changeset |
files
|
Fri, 24 Oct 1997 17:17:10 +0200 |
wenzelm |
self_ref: check_stale;
|
changeset |
files
|
Fri, 24 Oct 1997 17:15:59 +0200 |
wenzelm |
eq_thm (from drule.ML);
|
changeset |
files
|
Fri, 24 Oct 1997 17:14:41 +0200 |
wenzelm |
added declared: T -> string -> bool;
|
changeset |
files
|
Fri, 24 Oct 1997 17:14:02 +0200 |
wenzelm |
Pure.thy;
|
changeset |
files
|
Fri, 24 Oct 1997 17:13:21 +0200 |
wenzelm |
ProtoPure.thy;
|
changeset |
files
|
Fri, 24 Oct 1997 17:12:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 24 Oct 1997 17:12:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 24 Oct 1997 17:11:48 +0200 |
wenzelm |
removed add_thms_as_axms;
|
changeset |
files
|
Fri, 24 Oct 1997 17:11:23 +0200 |
wenzelm |
Init 'theorems' data. The Pure theories.
|
changeset |
files
|
Fri, 24 Oct 1997 17:07:34 +0200 |
wenzelm |
added pure_thy.ML;
|
changeset |
files
|
Fri, 24 Oct 1997 17:06:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 24 Oct 1997 11:56:12 +0200 |
nipkow |
Modified comment.
|
changeset |
files
|
Fri, 24 Oct 1997 11:24:21 +0200 |
nipkow |
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
|
changeset |
files
|
Fri, 24 Oct 1997 11:05:21 +0200 |
nipkow |
HOL/Map
|
changeset |
files
|
Fri, 24 Oct 1997 10:31:31 +0200 |
nipkow |
Added the new theory Map.
|
changeset |
files
|
Thu, 23 Oct 1997 12:49:16 +0200 |
wenzelm |
added record section;
|
changeset |
files
|
Thu, 23 Oct 1997 12:48:48 +0200 |
wenzelm |
Sign.name_of;
|
changeset |
files
|
Thu, 23 Oct 1997 12:47:59 +0200 |
wenzelm |
Sign.stamp_names_of;
|
changeset |
files
|
Thu, 23 Oct 1997 12:44:46 +0200 |
wenzelm |
improved typ parser, exported;
|
changeset |
files
|
Thu, 23 Oct 1997 12:43:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 23 Oct 1997 12:13:15 +0200 |
wenzelm |
hide id, stamps;
|
changeset |
files
|
Thu, 23 Oct 1997 12:10:55 +0200 |
wenzelm |
Sign.stamp_names_of;
|
changeset |
files
|
Thu, 23 Oct 1997 12:10:32 +0200 |
wenzelm |
added sort_wrt;
|
changeset |
files
|
Thu, 23 Oct 1997 12:09:48 +0200 |
wenzelm |
fixed prune of hidden short names;
|
changeset |
files
|
Thu, 23 Oct 1997 12:09:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 22 Oct 1997 11:36:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 22 Oct 1997 11:36:29 +0200 |
wenzelm |
certify: check_stale;
|
changeset |
files
|
Tue, 21 Oct 1997 18:15:43 +0200 |
wenzelm |
improved handling of draft signatures / theories; draft thms (and
|
changeset |
files
|
Tue, 21 Oct 1997 18:09:13 +0200 |
wenzelm |
sg_ref: automatic adjustment of thms of draft theories;
|
changeset |
files
|
Tue, 21 Oct 1997 17:48:06 +0200 |
wenzelm |
commit;
|
changeset |
files
|
Tue, 21 Oct 1997 17:47:50 +0200 |
wenzelm |
made Poly/ML happy, but SML/NJ unhappy;
|
changeset |
files
|
Tue, 21 Oct 1997 17:38:31 +0200 |
nipkow |
typo
|
changeset |
files
|
Tue, 21 Oct 1997 17:36:54 +0200 |
nipkow |
Corrected alphabetical order of entries in signature.
|
changeset |
files
|