isabelle: Graph

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

tuned;
1997-02-07, by wenzelm
Modified proofs due to added triv_forall_equality.
1997-02-07, by nipkow
Modified proofs because of added "triv_forall_equality".
1997-02-07, by nipkow
Added "triv_forall_equality" to HOL_ss.
1997-02-07, by nipkow
functionality added to getsettings;
1997-02-06, by wenzelm
removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06, by wenzelm
removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06, by wenzelm
removed getplatform;
1997-02-06, by wenzelm
integrated getplatform stuff;
1997-02-06, by wenzelm
now falls back on ucat instead of cat;
1997-02-06, by wenzelm
improved usage msg;
1997-02-06, by wenzelm
added eq_sort (will move to sorts.ML eventually);
1997-02-06, by wenzelm
adapted to new Syntax.read_typ;
1997-02-06, by wenzelm
adapted read_typ, simple_read_typ;
1997-02-06, by wenzelm
improved comments;
1997-02-06, by wenzelm
added string_of_vname' (treats neg. index as free);
1997-02-06, by wenzelm
cd made readably again;
1997-02-06, by wenzelm
tuned;
1997-02-05, by wenzelm
Gradual switching to Basis Library functions nth, drop, etc.
1997-02-04, by paulson
now uses tee -i instead of perl;
1997-02-04, by wenzelm
now uses ISABELLE_INSTALLFONTS;
1997-02-04, by wenzelm
added ISABELLE_INSTALLFONTS;
1997-02-04, by wenzelm
Declaration of ccontr (classical contradiction) for HOL compatibility
1997-01-31, by paulson
Correction to Problem 24
1997-01-31, by paulson
Correction to Problem 24
1997-01-31, by paulson
Correction to Problem 24 (with unsatisfactory proof)
1997-01-31, by paulson
ex_impE was incorrectly listed as Safe
1997-01-31, by paulson
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
1997-01-31, by oheimb
added Classlib.* and Witness.*,
1997-01-31, by oheimb
moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex,
1997-01-31, by oheimb
added def_fix_ind and def_wfix_ind for convenience
1997-01-31, by oheimb
added addloop (and also documentation of addsolver
1997-01-31, by oheimb
changed handling of cont_lemmas and adm_lemmas
1997-01-31, by oheimb
fixed getplatform call;
1997-01-29, by wenzelm
removed warning for unprintable chars in strings (functionality will
1997-01-29, by wenzelm
The redeclaration of qed_spec_mp is unnecessary because it is now declared
1997-01-29, by paulson
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
1997-01-29, by paulson
fixed problems with strange user .bashrc etc. (stty, ...);
1997-01-28, by wenzelm
Tidied unicity theorems
1997-01-27, by paulson
deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!
1997-01-27, by paulson
Corrected faulty comment
1997-01-27, by paulson
More news items, dating back to 1995
1997-01-27, by paulson
*** empty log message ***
1997-01-27, by wenzelm
*** empty log message ***
1997-01-24, by wenzelm
*** empty log message ***
1997-01-24, by wenzelm
Isabelle NEWS -- history of user-visible changes;
1997-01-24, by wenzelm
changed case symbol to \<Rightarrow>;
1997-01-24, by wenzelm
'rm -f' instead of 'mv -f';
1997-01-23, by wenzelm
Re-ordering of certificates so that session keys appear in decreasing order
1997-01-23, by paulson
Cosmetic improvements
1997-01-23, by paulson
'rm -f' instead of 'cp -f';
1997-01-23, by wenzelm
tuned;
1997-01-23, by wenzelm
expand shorthand goal commands;
1997-01-23, by wenzelm
added AxClasses test;
1997-01-23, by wenzelm
replaces README;
1997-01-23, by wenzelm
dummy file required for proper HTML generation;
1997-01-23, by wenzelm
removed;
1997-01-23, by wenzelm
removed \<mu> syntax;
1997-01-23, by wenzelm
added symbols syntax;
1997-01-23, by wenzelm
turned some consts into syntax;
1997-01-23, by wenzelm
Mended spelling error
1997-01-23, by paulson
Added sees_Spy_partsEs
1997-01-23, by paulson
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
1997-01-23, by paulson
Added warning msg when the simplifier cannot use a premise as a rewrite rule
1997-01-22, by nipkow
Modified MiniML. Added W0.
1997-01-21, by nipkow
Simplified proofs
1997-01-21, by paulson
Improved layout and updated comments
1997-01-21, by paulson
Improved text.
1997-01-20, by nipkow
Now requests runtimes of all theories
1997-01-20, by paulson
Simplified Oops case of main theorem
1997-01-20, by paulson
Documents the new command "prlim"
1997-01-20, by paulson
Added W0 and modified MiniML.
1997-01-17, by nipkow
Ball_Un -> ball_Un
1997-01-17, by nipkow
The new version of MiniML including "let".
1997-01-17, by nipkow
Algorithm I has not been ported to the polymorphic version yet.
1997-01-17, by nipkow
Updated documentation pointers.
1997-01-17, by nipkow
added gen_overwrite;
1997-01-17, by wenzelm
addsimps, addeqcongs: replaced @ by gen_union;
1997-01-17, by wenzelm
Incorporated Larry's changes.
1997-01-17, by nipkow
New rewrites for bounded quantifiers
1997-01-17, by paulson
This is the old version og MiniML for the monomorphic case.
1997-01-17, by nipkow
Modified some defs and shortened proofs.
1997-01-17, by nipkow
Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-17, by paulson
Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
1997-01-17, by paulson
Added the prlim command
1997-01-17, by paulson
New miniscoping rules for the bounded quantifiers and UN/INT operators
1997-01-17, by paulson
Got rid of Alls in List.
1997-01-17, by nipkow
Got rid of Alls in favour of !x:set_of_list
1997-01-17, by nipkow
binary oprations and relations;
1997-01-16, by wenzelm
added termless parameter;
1997-01-16, by wenzelm
added term order;
1997-01-16, by wenzelm
improved error msg;
1997-01-13, by wenzelm
added datatype order;
1997-01-13, by wenzelm
added -? option;
1997-01-13, by wenzelm
replaced unit refs by 'stamp';
1997-01-13, by wenzelm
cleaned up (real changes next time);
1997-01-10, by wenzelm
make all Isabelle systems afresh;
1997-01-09, by wenzelm
*** empty log message ***
1997-01-09, by wenzelm
IsaMakefile for ZF;
1997-01-09, by wenzelm
Tidying of proofs. New theorems are enterred immediately into the
1997-01-09, by paulson
New theorem add_leE
1997-01-09, by paulson
New treatment of nonce creation
1997-01-09, by paulson
Removal of needless "addIs [equality]", etc.
1997-01-09, by paulson
New discussion of implicit simpsets & clasets
1997-01-08, by paulson
IsaMakefile for HOLCF;
1997-01-08, by wenzelm
Removal of sum_cs and eq_cs
1997-01-08, by paulson
IsaMakefile for Sequents;
1997-01-08, by wenzelm
IsaMakefile for CTT;
1997-01-08, by wenzelm
IsaMakefile for FOLP;
1997-01-08, by wenzelm
IsaMakefile for CCL;
1997-01-08, by wenzelm
IsaMakefile for LCF;
1997-01-08, by wenzelm
IsaMakefile for Cube;
1997-01-08, by wenzelm
Removed some (not all!) uses of FOL_cs
1997-01-08, by paulson
Simplification of some proofs, especially by eliminating
1997-01-07, by paulson
Incorporation of HPair into Message
1997-01-07, by paulson
Default rewrite rules for quantification over Collect(A,P)
1997-01-07, by paulson
Default rewrite rules for quantification over Collect(A,P)
1997-01-07, by paulson
Now uses HPair
1997-01-07, by paulson
Tidied up the unicity proofs
1997-01-07, by paulson
Updated account of implicit simpsets and clasets
1997-01-07, by paulson