isabelle: Graph

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

Added comments
1997-11-28, by paulson
New timing functions startTiming and endTiming
1997-11-28, by paulson
addsplits now in FOL, ZF too
1997-11-28, by paulson
New example
1997-11-28, by paulson
Printing of statistics including time for search & reconstruction
1997-11-28, by paulson
New example
1997-11-28, by paulson
Removed dead code.
1997-11-28, by nipkow
Moved the quantifier elimination simp procs into Provers.
1997-11-28, by nipkow
Quantifier elimination procs.
1997-11-28, by nipkow
Fixed the definition of `termord': is now antisymmetric.
1997-11-28, by nipkow
several minor updates;
1997-11-27, by wenzelm
SYNC;
1997-11-27, by wenzelm
removed read_cterms;
1997-11-27, by wenzelm
fixed warning;
1997-11-27, by wenzelm
removed same_thm;
1997-11-27, by wenzelm
Tidying, mostly indentation
1997-11-27, by paulson
Deleted some needless addSIs; got rid of a slow Blast_tac
1997-11-27, by paulson
mk_norm_sum;
1997-11-27, by wenzelm
separate lists of simprocs;
1997-11-26, by wenzelm
Added rule impCE'
1997-11-26, by paulson
Blast_tac can prove Pelletier\'s problem 46\!
1997-11-26, by paulson
Tidying and using equalityCE instead of the slower equalityE
1997-11-26, by paulson
The change from iffE to iffCE means fewer case splits in most cases. Very few
1997-11-26, by paulson
Tidying
1997-11-26, by paulson
Tidying and modification to cope with iffCE
1997-11-26, by paulson
Added rule impCE'
1997-11-26, by paulson
Changes to AddIs improve performance of Blast_tac
1997-11-26, by paulson
Statistics
1997-11-26, by paulson
updated comment
1997-11-26, by paulson
Tidying and modification to cope with iffCE
1997-11-26, by paulson
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
1997-11-26, by wenzelm
added Arith provers;
1997-11-26, by wenzelm
Setup various arithmetic proof procedures.
1997-11-26, by wenzelm
added dest_nat;
1997-11-26, by wenzelm
moved to Arith/;
1997-11-26, by wenzelm
Cancel common constant factor from balanced exression.
1997-11-26, by wenzelm
Cancel common summands of balanced expressions.
1997-11-26, by wenzelm
removed conv_prover;
1997-11-26, by wenzelm
tuned;
1997-11-26, by wenzelm
added crep_cterm;
1997-11-26, by wenzelm
fixed type of thms_containing;
1997-11-26, by wenzelm
added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
1997-11-26, by wenzelm
cleaned signature;
1997-11-26, by wenzelm
removed merge_opts;
1997-11-26, by wenzelm
managed merge details;
1997-11-25, by mueller
resolved merge conflict;
1997-11-25, by mueller
Added read_def_cterms for simultaneous reading/typing of terms under
1997-11-24, by nipkow
fixed warning;
1997-11-22, by wenzelm
made SML/NJ happy;
1997-11-22, by wenzelm
tuned;
1997-11-22, by wenzelm
replaced by seq.ML;
1997-11-21, by wenzelm
changed Pure/Sequence interface;
1997-11-21, by wenzelm
SYNC;
1997-11-21, by wenzelm
cd, use: path variables;
1997-11-21, by wenzelm
comment;
1997-11-21, by wenzelm
obsolete;
1997-11-21, by wenzelm
changed Pure/Sequence interface -- isatool fixseq;
1997-11-21, by wenzelm
changed Sequence interface (now Seq, in seq.ML);
1997-11-21, by wenzelm
cd, use etc. now support path variables;
1997-11-21, by wenzelm
fix references to obsolete Pure/Sequence structure;
1997-11-21, by wenzelm
tidying
1997-11-21, by paulson
analz_mono_contra_tac was wrong
1997-11-21, by paulson
Deleted some useless comments
1997-11-21, by paulson
minor improvements of formulation and proofs
1997-11-21, by oheimb
corrected INDUCT_FILES
1997-11-21, by oheimb
$ISABELLE_HOME/src;
1997-11-20, by wenzelm
improved error msg;
1997-11-20, by wenzelm
removed old note;
1997-11-20, by wenzelm
adapted print methods;
1997-11-20, by wenzelm
improved theorems print method: transfer_sg;
1997-11-20, by wenzelm
init_data: improved print method;
1997-11-20, by wenzelm
removed data.ML (made part of sign.ML);
1997-11-20, by wenzelm
added type object = exn;
1997-11-20, by wenzelm
added transfer_sg;
1997-11-20, by wenzelm
fixed xstr token encoding;
1997-11-20, by wenzelm
tuned infer_types interface;
1997-11-20, by wenzelm
tuned infer_types interface;
1997-11-20, by wenzelm
moved Sign.print_sg to display.ML;
1997-11-20, by wenzelm
exported pretty_classrel, pretty_arity;
1997-11-20, by wenzelm
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
1997-11-20, by wenzelm
added implode_xstr: string list -> string, explode_xstr: string -> string list;
1997-11-20, by wenzelm
Now uses induct_tac
1997-11-20, by paulson
Updated the NatSum example
1997-11-20, by paulson
New, higher-level definition of \\out macro
1997-11-20, by paulson
Speeded up the proof of succ_lt_induct_lemma
1997-11-20, by paulson
Two new rewrites
1997-11-20, by paulson
Got rid of some slow deepen_tac calls
1997-11-20, by paulson
Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-20, by paulson
No more makeatletter/other
1997-11-20, by paulson
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
1997-11-18, by paulson
The dtac was discarding information, though apparently no proofs were hurt
1997-11-18, by paulson
Fixed bug in inst_split.
1997-11-18, by berghofe
improved big_rec_name lookup;
1997-11-17, by wenzelm
Updated comments. A bug causes MLWorks to use much
1997-11-17, by paulson
Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
1997-11-17, by paulson
Tuned function mk_cntxt_splitthm.
1997-11-17, by berghofe
Removed
1997-11-16, by nipkow
Redesigned the decision procedures for (Abelian) groups and commutative rings.
1997-11-15, by nipkow
Added
1997-11-15, by nipkow
merge_refs: check for different versions of theories;
1997-11-14, by wenzelm
export read_raw_typ;
1997-11-13, by wenzelm
fixed record parser;
1997-11-13, by wenzelm
improved record syntax;
1997-11-13, by wenzelm
made SML/NJ happy;
1997-11-13, by wenzelm
added thin_refl to hyp_subst_tac
1997-11-12, by oheimb
refer to $ISABELLE_HOME/src;
1997-11-12, by wenzelm
structure BasisLibrary;
1997-11-12, by wenzelm
renamed to use.ML;
1997-11-12, by wenzelm
Redefine 'use' command in order to support path variable expansion,
1997-11-12, by wenzelm
adapted to new Use, File structs;
1997-11-12, by wenzelm
added path variables;
1997-11-12, by wenzelm
File system operations.
1997-11-12, by wenzelm
moved old file stuff from library.ML to Thy/browser_info.ML;
1997-11-12, by wenzelm
added file.ML, use.ML;
1997-11-12, by wenzelm
tuned warning msg;
1997-11-12, by wenzelm
major cleanup;
1997-11-12, by wenzelm
moved 'latex' from library.ML to goals.ML;
1997-11-12, by wenzelm
tuned prths;
1997-11-12, by wenzelm
structure BasisLibrary;
1997-11-12, by wenzelm
added Thy/file.ML, Thy/use.ML;
1997-11-12, by wenzelm