isabelle: Graph

adapted to new implicit simpset;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
fixed thy dependencies;
1997-11-03, by wenzelm
aded thy_data;
1997-11-03, by wenzelm
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
Fixed the index entries for "recursion, general"
1997-10-21, by paulson
Many minor speedups:
1997-10-21, by paulson
New rewrite rules image_iff
1997-10-21, by paulson
Documented `addsplits'
1997-10-20, by nipkow
make SML/NJ happy;
1997-10-20, by wenzelm
rm IOA TLA;
1997-10-20, by wenzelm
tuned types;
1997-10-20, by wenzelm
tuned sig;
1997-10-20, by wenzelm
reset global_names;
1997-10-20, by wenzelm
set global_names;
1997-10-20, by wenzelm
replaced ops by consts;
1997-10-20, by wenzelm
removed Dlist;
1997-10-20, by wenzelm
\label{simp-chap} -> chap:simplification
1997-10-20, by nipkow
fixed goal_XXX;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
tuned;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
lookup long names of types;
1997-10-20, by wenzelm
tuned qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
qualified names;
1997-10-20, by wenzelm
local;
1997-10-20, by wenzelm
Sign.base_name;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
tuned output;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
Sign.base_name;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
local;
1997-10-20, by wenzelm
local section;
1997-10-20, by wenzelm
addsplits
1997-10-18, by nipkow
adapted to qualified names;
1997-10-17, by wenzelm
no longer tries bogus eta-contract involving aprops;
1997-10-17, by wenzelm
adapted to qualified names;
1997-10-17, by wenzelm
fixed RAW target;
1997-10-17, by wenzelm
(co) inductive / datatype package adapted to qualified names;
1997-10-17, by wenzelm
obselete 'end' hack;
1997-10-17, by wenzelm
global;
1997-10-17, by wenzelm
tuned "." syntax;
1997-10-17, by wenzelm
removed Classlib;
1997-10-17, by wenzelm
*** empty log message ***
1997-10-17, by wenzelm
setloop split_tac -> addsplits
1997-10-17, by nipkow
Added error messages.
1997-10-17, by nipkow
A lot of new comments
1997-10-17, by paulson
Eta-expanded a function decl to make sml/nj happy
1997-10-17, by paulson
Added "op" before "occs" to make sml/nj happy
1997-10-17, by paulson
New rewrite rules for simplifying conditionals
1997-10-17, by paulson
New trivial rewrites
1997-10-17, by paulson
New rewrite rules for simplifying conditionals
1997-10-17, by paulson
Better simplification eliminates a command from proof of psubset_card
1997-10-17, by paulson
New simprules imp_disj1,2 and some comments
1997-10-17, by paulson
Added image_eqI to simpset.
1997-10-17, by nipkow
Removed image_eqI from simpset because of clash with neq_shrK.
1997-10-17, by nipkow
AddIffs [all_not_in_conv];
1997-10-16, by nipkow
global;
1997-10-16, by wenzelm
Modified comment.
1997-10-16, by nipkow
New simprules imp_disj1, imp_disj2
1997-10-16, by paulson
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
1997-10-16, by paulson
Removed comment.
1997-10-16, by nipkow
tuned;
1997-10-16, by wenzelm
removed begin;
1997-10-16, by wenzelm
fixed prep_ext;
1997-10-16, by wenzelm
Simplified proof.
1997-10-16, by nipkow
Simplified proof because of better simplifier.
1997-10-16, by nipkow
Various new lemmas. Improved conversion of equations to rewrite rules:
1997-10-16, by nipkow
added transfer: theory -> thm -> thm;
1997-10-16, by wenzelm
oops;
1997-10-16, by wenzelm
The simplifier has been improved a little: equations s=t which used to be
1997-10-16, by nipkow
fixed dependencies;
1997-10-16, by wenzelm
transfer thy Ord_nat;
1997-10-16, by wenzelm
sevaral goals restated in mono.thy;
1997-10-16, by wenzelm
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
1997-10-16, by wenzelm
transfer InfDatatype.thy Limit_VfromE;
1997-10-16, by wenzelm
transfer CardinalArith.thy nat_into_Ord;
1997-10-16, by wenzelm
improved pretty_arity;
1997-10-16, by wenzelm
added merge_theories (new name arg);
1997-10-16, by wenzelm
fixed merge_theories;
1997-10-16, by wenzelm
revert to 1.3;
1997-10-16, by wenzelm
revert to 1.1;
1997-10-16, by wenzelm
Added last, butlast, dropped ttl.
1997-10-16, by nipkow
lala
1997-10-16, by mueller
Eta-expansion of function declarations, for value polymorphism
1997-10-16, by paulson
remove merge_theories;
1997-10-15, by wenzelm
make_draft replaced by prep_ext;
1997-10-15, by wenzelm
tuned;
1997-10-15, by wenzelm
eliminated aliasing merge: now always extends;
1997-10-15, by wenzelm
tuned comment;
1997-10-15, by wenzelm
improved print_data;
1997-10-15, by wenzelm
tuned;
1997-10-15, by wenzelm
slightly changed interfaces for oracles;
1997-10-15, by wenzelm
Added ack to Mateja Jamnik.
1997-10-15, by nipkow
tuned;
1997-10-15, by wenzelm
tuned;
1997-10-14, by wenzelm
added additional generic data;
1997-10-14, by wenzelm
Sign.print_data;
1997-10-14, by wenzelm
added init_data, get_data, put_data;
1997-10-14, by wenzelm
added data.ML;
1997-10-14, by wenzelm
Arbitrarily typed data.
1997-10-14, by wenzelm