isabelle: Graph

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

manual steps comment;
1997-02-17, by wenzelm
*** empty log message ***
1997-02-17, by wenzelm
described changes for HOLCF-Version without rules and arities
1997-02-17, by slotosch
file moved;
1997-02-17, by wenzelm
file moved here;
1997-02-17, by wenzelm
configure - adapt Isabelle distribution to system environment
1997-02-17, by wenzelm
improved description of recent changes
1997-02-17, by oheimb
reflecting recent changes of the simplifier
1997-02-17, by slotosch
corrected type of plift
1997-02-17, by oheimb
reflecting recent changes of the simplifier
1997-02-17, by oheimb
mk_rews: automatically includes strip_shyps, zero_var_indexes;
1997-02-17, by wenzelm
New file for theorems of Porder0
1997-02-17, by slotosch
tuned comments;
1997-02-17, by wenzelm
Examples are adopted to the changes from HOLCF.
1997-02-17, by slotosch
using types one = unit lift and translations causes troubles between
1997-02-17, by slotosch
Changes of HOLCF from Oscar Slotosch:
1997-02-17, by slotosch
*** empty log message ***
1997-02-15, by oheimb
reflecting my recent changes of the classical reasoner
1997-02-15, by oheimb
reflecting my recent changes of the simplifier and classical reasoner
1997-02-15, by oheimb
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
1997-02-15, by oheimb
cosmetic
1997-02-15, by oheimb
updated mini_ss
1997-02-15, by oheimb
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
1997-02-15, by oheimb
corrected minor mistakes
1997-02-15, by oheimb
description of safe vs. unsafe wrapper and the functions involved
1997-02-15, by oheimb
moved THEN_MAYBE to Pure/tctical.ML
1997-02-15, by oheimb
added deleqcongs, richer rep_ss
1997-02-15, by oheimb
description of del(eq)congs, safe and unsafe solver
1997-02-15, by oheimb
added THEN_MAYBE and THEN_MAYBE'
1997-02-15, by oheimb
added del_congs
1997-02-15, by oheimb
Some lemmas changed to valuesd
1997-02-14, by narasche
fixed comment;
1997-02-14, by wenzelm
improved interface options;
1997-02-14, by wenzelm
semi fix of piping-quit peoblem (should work on systems with *real* sh);
1997-02-14, by wenzelm
globally unset ENV, BASH_ENV;
1997-02-14, by wenzelm
Made troublesome simplifier warning dependent on trace_simp.
1997-02-14, by nipkow
Modified and shortened adm_disj lemmas.
1997-02-14, by nipkow
Deleted a useless definition
1997-02-14, by paulson
Added optimization: do nothing for empty list
1997-02-14, by paulson
A bit more pattern-matching in eta_contract
1997-02-14, by paulson
Tidying and a corrected comment
1997-02-14, by paulson
Added a new challenge problem
1997-02-14, by paulson
Updated documentation of IFOL_ss
1997-02-14, by paulson
Documented thin_tac
1997-02-14, by paulson
Strengthened warnings concerning topthm(), etc.
1997-02-14, by paulson
Updated a reference
1997-02-14, by paulson
New class "order" and accompanying changes.
1997-02-12, by nipkow
New class "order" and accompanying changes.
1997-02-12, by nipkow
TFL: missing -q option!
1997-02-12, by wenzelm
tuned names: partial order, linear order;
1997-02-12, by wenzelm
tuned startup;
1997-02-10, by wenzelm
fixed comment;
1997-02-10, by wenzelm
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-02-10, by paulson
Renamed structure Int (intuitionistic prover) to IntPr
1997-02-10, by paulson
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-02-10, by paulson
removed ISABELLE_INTERFACE_OPTIONS;
1997-02-07, by wenzelm
tuned;
1997-02-07, by wenzelm
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