isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

HOL theory data.
1997-11-03, by wenzelm
added thy_data.ML;
1997-11-03, by wenzelm
new implicit simpset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
new implicit claset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
adapted to new implicit claset mechanism;
1997-11-03, by wenzelm
fix references to implicit claset and simpset;
1997-11-03, by wenzelm
do not overwrite backup files;
1997-11-03, by wenzelm
set_session renamed to add_session;
1997-11-03, by wenzelm
tuned error msg;
1997-11-03, by wenzelm
made SML/97 happy;
1997-11-03, by wenzelm
expand_option_bind -> split_option_bind
1997-11-03, by nipkow
expand_option_case -> split_option_case
1997-11-03, by nipkow
*** empty log message ***
1997-11-03, by nipkow
expand_list_case -> split_list_case
1997-11-03, by nipkow
Indexed split_t_case.
1997-11-02, by nipkow
Documented `split_t_case' thm genearted by datatype.
1997-11-02, by nipkow
Fixed comments
1997-11-01, by paulson
New treatment of overloading\!
1997-11-01, by paulson
New syntax function for types
1997-11-01, by paulson
Faster lexing
1997-11-01, by paulson
New way of referring to Basis Library
1997-11-01, by paulson
mended type constraint\!
1997-11-01, by paulson
Set.thy was too specific
1997-11-01, by paulson
New Blast_tac (and minor tidying...)
1997-11-01, by paulson
Auto update
1997-11-01, by paulson
propagate exn msg;
1997-11-01, by wenzelm
dup sections: warning instead of error;
1997-10-31, by wenzelm
Session, Context;
1997-10-31, by wenzelm
tuned;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-31, by wenzelm
*** empty log message ***
1997-10-31, by wenzelm
added str_of_sg: sg -> string;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-30, by wenzelm
tuned thy_data;
1997-10-30, by wenzelm
tuned init_data;
1997-10-30, by wenzelm
added thy_data;
1997-10-30, by wenzelm
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
1997-10-30, by wenzelm
Modified trace output routines of simplifier.
1997-10-30, by nipkow
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
PureThy.add_store_defs_i, PureThy.add_store_axioms;
1997-10-30, by wenzelm
fixed try_dest_adm;
1997-10-30, by wenzelm
added adm.ML;
1997-10-30, by wenzelm
tuned;
1997-10-30, by wenzelm
tuned simp trace;
1997-10-30, by wenzelm
*** empty log message ***
1997-10-30, by nipkow
Removed spurious blank.
1997-10-30, by nipkow
Updated proofs
1997-10-30, by nipkow
For each datatype `t' there is now a theorem `split_t_case' of the form
1997-10-30, by nipkow
fixed spaces in qed;
1997-10-29, by wenzelm
debugging concerning sort variables
1997-10-29, by oheimb
PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i, PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i;
1997-10-28, by wenzelm
PureThy.add_store_axioms;
1997-10-28, by wenzelm
fixed qed;
1997-10-28, by wenzelm
do not change global_names flag;
1997-10-28, by wenzelm
restructured -- uses PureThy storage facilities;
1997-10-28, by wenzelm
added ignored_consts, thms_containing, add_store_axioms(_i),
1997-10-28, by wenzelm
always reload .ML *and* .thy file;
1997-10-28, by wenzelm
PureThy.add_store_defs, PureThy.add_store_axioms;
1997-10-28, by wenzelm
added ancestors;
1997-10-28, by wenzelm
added name_of_thm;
1997-10-28, by wenzelm
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
1997-10-28, by wenzelm
eq_thm moved to thm.ML;
1997-10-28, by wenzelm
add_store_axioms_i;
1997-10-28, by wenzelm
Added finite_UNION/SigmaI.
1997-10-28, by nipkow
oops;
1997-10-27, by wenzelm
renamed put_* to store_*;
1997-10-27, by wenzelm
flipped global_names default;
1997-10-27, by wenzelm
do not change global_names flag;
1997-10-27, by wenzelm
Isa94-2 instead of Isa95;
1997-10-27, by wenzelm
adapted domain and ax_ops package for name spaces
1997-10-27, by oheimb
made SML/NJ happy;
1997-10-27, by wenzelm
Deleted two needless theorems
1997-10-27, by paulson
internalized some names
1997-10-25, by oheimb
corrected two comments
1997-10-25, by oheimb
Added
1997-10-24, by nipkow
oops, swap warnings;
1997-10-24, by wenzelm
record: tuned output;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
merge: default to ProtoPure.thy;
1997-10-24, by wenzelm
ProtoPure.thy etc.;
1997-10-24, by wenzelm
tuned names;
1997-10-24, by wenzelm
self_ref: check_stale;
1997-10-24, by wenzelm
eq_thm (from drule.ML);
1997-10-24, by wenzelm
added declared: T -> string -> bool;
1997-10-24, by wenzelm
Pure.thy;
1997-10-24, by wenzelm
ProtoPure.thy;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
removed add_thms_as_axms;
1997-10-24, by wenzelm
Init 'theorems' data. The Pure theories.
1997-10-24, by wenzelm
added pure_thy.ML;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
Modified comment.
1997-10-24, by nipkow
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
1997-10-24, by nipkow
HOL/Map
1997-10-24, by nipkow
Added the new theory Map.
1997-10-24, by nipkow
added record section;
1997-10-23, by wenzelm
Sign.name_of;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
improved typ parser, exported;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
hide id, stamps;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
added sort_wrt;
1997-10-23, by wenzelm
fixed prune of hidden short names;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
tuned;
1997-10-22, by wenzelm
certify: check_stale;
1997-10-22, by wenzelm
improved handling of draft signatures / theories; draft thms (and
1997-10-21, by wenzelm
sg_ref: automatic adjustment of thms of draft theories;
1997-10-21, by wenzelm
commit;
1997-10-21, by wenzelm
made Poly/ML happy, but SML/NJ unhappy;
1997-10-21, by wenzelm
typo
1997-10-21, by nipkow
Corrected alphabetical order of entries in signature.
1997-10-21, by nipkow