isabelle: Graph

renamed rep_claset to rep_cs
1998-02-25, by oheimb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
1998-02-25, by oheimb
changed wrapper mechanism of classical reasoner
1998-02-25, by oheimb
added split_all_tac to claset()
1998-02-25, by oheimb
changed wrapper mechanism of classical reasoner
1998-02-25, by oheimb
New theory of the inverse image of a function
1998-02-24, by paulson
Added some lemmas.
1998-02-24, by nipkow
Catches bad elim rules, handling exception OPTION
1998-02-23, by paulson
New laws for union
1998-02-23, by paulson
New laws for id
1998-02-23, by paulson
New induction schemas for lists (length and snoc).
1998-02-22, by nipkow
*** empty log message ***
1998-02-20, by nipkow
Congruence rules use == in premises now.
1998-02-20, by nipkow
Congruence rules use == in premises now.
1998-02-20, by nipkow
minor improvements
1998-02-20, by oheimb
re-arranged bindings for many function keys
1998-02-20, by oheimb
extended input syntax to handle names of special keys
1998-02-20, by oheimb
moved Ctrl entry before Alt entry
1998-02-20, by oheimb
New theorem eq_imp_le
1998-02-20, by paulson
Four new Union/Intersection laws
1998-02-19, by paulson
corrected problem with auto_tac: now uses a variant of depth_tac that avoids
1998-02-18, by oheimb
added New Jersey mirror;
1998-02-18, by wenzelm
Improved loop-test for rewrite rules a little.
1998-02-18, by nipkow
tuned comment;
1998-02-18, by wenzelm
added append (curried);
1998-02-13, by wenzelm
*** empty log message ***
1998-02-12, by wenzelm
Sign.merge vs. Sign.nontriv_merge;
1998-02-12, by wenzelm
tuned comments;
1998-02-12, by wenzelm
oops;
1998-02-12, by wenzelm
tuned print_cs;
1998-02-12, by wenzelm
updated;
1998-02-12, by wenzelm
tuned;
1998-02-12, by wenzelm
added explicit signature;
1998-02-12, by wenzelm
improved comments;
1998-02-12, by wenzelm
fixed add_trrules: intern root;
1998-02-12, by wenzelm
export map_trrule;
1998-02-12, by wenzelm
tuned add_trrules;
1998-02-12, by wenzelm
improved is_letter etc.;
1998-02-12, by wenzelm
New Addsimps for Compl rules
1998-02-10, by paulson
New AddIffs le_0_eq and neq0_conv
1998-02-10, by paulson
Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
1998-02-09, by nipkow
Used THEN_ALL_NEW.
1998-02-09, by nipkow
moved freeze_thaw to drule.ML
1998-02-07, by paulson
Tidying; rotate_prems; moved freeze_thaw from tactic.ML
1998-02-07, by paulson
AC and other rewrite rules for Un and Int
1998-02-07, by paulson
auto update
1998-02-07, by paulson
Added reference to rotate_prems
1998-02-07, by paulson
filter_size -> length_filter
1998-02-06, by nipkow
Added `remdups'
1998-02-06, by nipkow
added Vartab: TABLE;
1998-02-06, by wenzelm
added param;
1998-02-05, by wenzelm
added THEN_ALL_NEW;
1998-02-05, by wenzelm
New theorem Image_id
1998-02-05, by paulson
New theorem order_eq_refl
1998-02-05, by paulson
New max, min theorems
1998-02-05, by paulson
Added some more explicit guarantees of key secrecy for agents
1998-02-05, by paulson
Fixed a lot of overfull and underfull lines (hboxes)
1998-02-05, by paulson
Updated the description of how to set up hyp_subst_tac
1998-02-05, by paulson
New example, Pow_Sigma_bij
1998-02-02, by paulson
fixed WWW links
1998-02-02, by paulson
Three new facts about Image
1998-02-02, by paulson
Replaced \\1 by $1 as Perl itself asked me to...
1998-02-02, by paulson
Fixed the description of recdef
1998-01-30, by paulson
tuned msgs;
1998-01-30, by wenzelm
improved tracing of rewrite rule application;
1998-01-30, by wenzelm
removed dead messy code;
1998-01-30, by wenzelm
added read_var;
1998-01-30, by wenzelm
tuned;
1998-01-30, by wenzelm
Updated MOD reference
1998-01-23, by paulson
added symbols syntax;
1998-01-21, by wenzelm
reorganized into individual theories;
1998-01-20, by wenzelm
tuned;
1998-01-19, by wenzelm
make images;
1998-01-19, by wenzelm
tuned URL;
1998-01-15, by wenzelm
polyml-3.1;
1998-01-15, by wenzelm
obsolete;
1998-01-15, by wenzelm
added thms wrt weakening and strengthening in Abstraction;
1998-01-14, by mueller
New Jersey inactive; Isabelle98
1998-01-14, by wenzelm
HOL/record;
1998-01-14, by wenzelm
error with instantiantion of sub-records removed
1998-01-14, by narasche
added record.ML;
1998-01-14, by wenzelm
tuned;
1998-01-14, by wenzelm
added unit and prod stuff;
1998-01-14, by wenzelm
fixed Id;
1998-01-14, by wenzelm
smlnj-110 factory default;
1998-01-14, by wenzelm
added of_sort;
1998-01-14, by wenzelm
added base_path;
1998-01-13, by wenzelm
added simulations files to IOA;
1998-01-13, by mueller
added forward simulation correectness;
1998-01-13, by mueller
Simplification: sel make and update make
1998-01-13, by narasche
added abstraction files;
1998-01-12, by mueller
added further IOA liles;
1998-01-12, by mueller
updated to Isabelle98;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
added files containing temproal logic and abstraction;
1998-01-12, by mueller
Delsimprocs nat_cancel;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
1998-01-12, by paulson
tuned;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
fixed author;
1998-01-12, by wenzelm
Simplified proofs by omitting PA = {|XA, ...|} from RA2
1998-01-10, by paulson
trivial tidy
1998-01-10, by paulson
tuned;
1998-01-09, by wenzelm
automatic index.html patch;
1998-01-09, by wenzelm
tuned;
1998-01-09, by wenzelm
tuned ISABELLE_TMP_PREFIX;
1998-01-09, by wenzelm
thm_ord;
1998-01-09, by wenzelm
eliminated make_ord;
1998-01-09, by wenzelm
ISABELLE_TMP_PREFIX: $LOGNAME
1998-01-09, by wenzelm
several minor updates;
1998-01-09, by wenzelm
tuned;
1998-01-08, by wenzelm
index.html for Isabelle Distribution Area;
1998-01-08, by wenzelm
updated to Isabelle98;
1998-01-08, by wenzelm
tuned;
1998-01-08, by wenzelm
fixed thm_less;
1998-01-08, by wenzelm
Expressed most Oops rules using Notes instead of Says, and other tidying
1998-01-08, by paulson
added split_paired_Ex to the implicit simpset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added newline at end of file
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by oheimb
streamlined specification of included theories
1998-01-08, by oheimb
corrected Title
1998-01-08, by oheimb
removed obsolete comment
1998-01-08, by oheimb
added Univalent
1998-01-08, by oheimb
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
1998-01-08, by oheimb
added update_same, update_other, update_triv, and map_of_SomeD
1998-01-08, by oheimb
replaced fn _ => by K
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by wenzelm
New rule: image_subset
1998-01-08, by paulson
Restored the ciphertext in OR4 in order to make the spec closer to that in
1998-01-08, by paulson
Tidied by adding more default simprules
1998-01-08, by paulson
adapted to new split order;
1998-01-07, by wenzelm
adapted to new sort function;
1998-01-07, by wenzelm
improved targets;
1998-01-07, by wenzelm
tuned;
1998-01-06, by wenzelm
added -u option (again);
1998-01-05, by wenzelm
Now calls Blast_tac more often
1998-01-05, by paulson
obsolete;
1998-01-02, by wenzelm
feeder;
1998-01-02, by wenzelm
Changed required by new blast_tac (the one that squashes flex-flex pairs)
1998-01-02, by paulson
Blast_tac now squashes flex-flex pairs immediately
1998-01-02, by paulson
New theorem image_subsetI
1998-01-02, by paulson
Making proofs faster, especially using keysFor_parts_insert
1998-01-02, by paulson
do require perl;
1998-01-02, by wenzelm
Auto_tac now has type tactic, not unit->tactic
1998-01-02, by paulson
Declared startTiming and endTiming
1998-01-02, by paulson
use feeder to pipe into ML;
1997-12-31, by wenzelm
removed -i option;
1997-12-31, by wenzelm
nth -> !
1997-12-30, by nipkow
nth -> !
1997-12-30, by nipkow
feed isabelle session;
1997-12-29, by wenzelm
commented out symboloutput.pl;
1997-12-29, by wenzelm
added feeder.pl;
1997-12-29, by wenzelm
pretty_name_space;
1997-12-29, by wenzelm
removed declared;
1997-12-29, by wenzelm
removed distinct_fst_string;
1997-12-29, by wenzelm
improved error handling;
1997-12-28, by wenzelm
fixed execute;
1997-12-28, by wenzelm
made MLWorks happy;
1997-12-28, by wenzelm
stderr to $LOG;
1997-12-28, by wenzelm
Symtab.empty;
1997-12-28, by wenzelm
improved internal representation;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
added >> : (theory -> theory) -> unit;
1997-12-28, by wenzelm
tuned;
1997-12-28, by wenzelm
replaced symtab.ML by table.ML;
1997-12-28, by wenzelm
renamed (is_)null to (is_)empty;
1997-12-28, by wenzelm
Generic tables (lacking delete operation). Implemented as 2-3 trees.
1997-12-27, by wenzelm
tuned;
1997-12-24, by wenzelm
export range_type;
1997-12-24, by wenzelm
improved comment;
1997-12-24, by wenzelm
More restrictive patterns to prevent changing comments
1997-12-24, by paulson
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-24, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Now Blast_tac works properly
1997-12-23, by paulson
Tidied. Also better proof using new blast_tac
1997-12-23, by paulson
Decremented subscript because of change to iffD1
1997-12-23, by paulson
Tidied using rev_iffD1, etc
1997-12-23, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Tidied using more default rules
1997-12-23, by paulson
Overloading info for image
1997-12-23, by paulson
tidied
1997-12-23, by paulson
New rules rev_iffD{1,2}
1997-12-23, by paulson
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-23, by paulson
New "obvious theorems"
1997-12-23, by paulson
Added range-type for completeness
1997-12-22, by paulson
New example
1997-12-22, by paulson
New rules rev_iffD{1,2}
1997-12-22, by paulson
corrected removal to /tmp/tmp.c
1997-12-19, by oheimb
added removal to /tmp/tmp.txt
1997-12-19, by oheimb
records without signature
1997-12-19, by narasche
remove signatrue from records
1997-12-19, by narasche
tuned;
1997-12-19, by wenzelm
new version;
1997-12-19, by wenzelm
added record.ML;
1997-12-19, by wenzelm
first version of records
1997-12-19, by narasche
pasted old insertion sort (does not work with new sort function!)
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
log file;
1997-12-19, by wenzelm
leading 0s;
1997-12-19, by wenzelm
tuned;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
log files;
1997-12-19, by wenzelm
tuned;
1997-12-19, by wenzelm
added rev_order, make_ord;
1997-12-19, by wenzelm
term order;
1997-12-19, by wenzelm
term order stuff moved to term.ML;
1997-12-19, by wenzelm
log file;
1997-12-19, by wenzelm
'clean' target;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
Term.termless;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
removed maketest;
1997-12-19, by wenzelm
showtime - print time.
1997-12-18, by wenzelm
added expand_split_asm
1997-12-18, by oheimb
UNIV_I no longer counts as safe
1997-12-18, by paulson
tuned;
1997-12-17, by wenzelm
added mlworks;
1997-12-17, by wenzelm
added MLWorks;
1997-12-17, by wenzelm
misc improvements;
1997-12-17, by wenzelm
tuned tmp file name;
1997-12-17, by wenzelm
tuned comment;
1997-12-17, by wenzelm
added ML-Systems/mlworks.ML;
1997-12-17, by wenzelm
MLWorks startup script (for 1.0r2 or later).
1997-12-16, by wenzelm
renamed to mlworks.ML;
1997-12-16, by wenzelm
Compatibility file for MLWorks version 1.0r2 or later.
1997-12-16, by wenzelm
expandshort;
1997-12-16, by wenzelm
Simplified proofs using rewrites for f``A where f is injective
1997-12-16, by paulson
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
1997-12-16, by paulson
obsolete;
1997-12-16, by wenzelm
tuned;
1997-12-16, by wenzelm
obsolete;
1997-12-16, by wenzelm
adapted from Larry's version;
1997-12-16, by wenzelm
improved;
1997-12-16, by wenzelm
improved COMMIT_RO;
1997-12-15, by wenzelm
tuned;
1997-12-15, by wenzelm