isabelle: Graph

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

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