Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-256
+256
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
polyml-3.1;
1997-12-15, by wenzelm
make smlnj-110 default;
1997-12-15, by wenzelm
tuned;
1997-12-15, by wenzelm
tuned;
1997-12-15, by wenzelm
No longer depend on theory context!
1997-12-15, by wenzelm
version = "Isabelle98: Jan 1998";
1997-12-13, by wenzelm
tuned comment;
1997-12-13, by wenzelm
smlnj-110;
1997-12-13, by wenzelm
deleted smlnj-1.09.ML;
1997-12-12, by wenzelm
obsolete;
1997-12-12, by wenzelm
Compatibility file for Standard ML of New Jersey.
1997-12-12, by wenzelm
tuned;
1997-12-12, by wenzelm
prepared for Isabelle98;
1997-12-12, by wenzelm
added;
1997-12-12, by wenzelm
obsolete;
1997-12-12, by wenzelm
tuned;
1997-12-12, by wenzelm
tuned msg;
1997-12-12, by wenzelm
tuned;
1997-12-12, by wenzelm
major update;
1997-12-12, by wenzelm
SYNC;
1997-12-12, by wenzelm
new blast_tac no longer works here
1997-12-12, by paulson
More deterministic (?) contr_tac
1997-12-12, by paulson
More deterministic and therefore faster (sometimes) proof reconstruction
1997-12-12, by paulson
ugly patch for new Blast_tac
1997-12-12, by paulson
Faster proof of mult_less_cancel2
1997-12-12, by paulson
tuned;
1997-12-11, by wenzelm
Tidied final proof
1997-12-11, by paulson
Tidied proof of finite_subset_induct
1997-12-11, by paulson
Got rid of mod2_neq_0
1997-12-11, by paulson
\subsection{*Theory inclusion};
1997-12-08, by wenzelm
Tidying to fix overfull lines, etc
1997-12-08, by paulson
Comprehensive (??) list of bugs, fixed or not
1997-12-08, by paulson
tuned;
1997-12-07, by wenzelm
added print_claset;
1997-12-07, by wenzelm
Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
1997-12-06, by nipkow
Got rid of some preds and replaced some n~=0 by 0<n.
1997-12-06, by nipkow
Cleaned up arithmetic mess.
1997-12-06, by nipkow
instantiate';
1997-12-05, by wenzelm
changed typed_print_translation;
1997-12-05, by wenzelm
tuned;
1997-12-05, by wenzelm
nat_cancel enabled by default;
1997-12-05, by wenzelm
adapted proofs to cope with simprocs nat_cancel;
1997-12-05, by wenzelm
improved arbitrary_def: we now really don't know nothing about it!
1997-12-05, by wenzelm
use_thy no longer requires writable current directory;
1997-12-05, by wenzelm
adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
1997-12-05, by wenzelm
simplification procedures nat_cancel enabled by default;
1997-12-05, by wenzelm
tmp_name;
1997-12-05, by wenzelm
added print_simpset;
1997-12-04, by wenzelm
added is_base;
1997-12-04, by wenzelm
added reset_context;
1997-12-04, by wenzelm
added eq_set;
1997-12-04, by wenzelm
moved global_names ref to Pure/ROOT.ML;
1997-12-04, by wenzelm
pred -> -1
1997-12-04, by nipkow
pred n -> n-1
1997-12-04, by nipkow
Simplified proofs.
1997-12-04, by nipkow
Added thm mult_div_cancel
1997-12-04, by nipkow
n ~= 0 should become 0 < n
1997-12-03, by nipkow
Replaced n ~= 0 by 0 < n
1997-12-03, by nipkow
pass return code!!
1997-12-03, by wenzelm
Fixed the treatment of substitution for equations, restricting occurrences of
1997-12-03, by paulson
updated for latest Blast_tac, which treats equality differently
1997-12-03, by paulson
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1997-12-03, by paulson
Tidying and some comments
1997-12-03, by paulson
updated for latest Blast_tac, which treats equality differently
1997-12-03, by paulson
Instantiated the one-point-rule quantifier simpprocs for FOL
1997-12-03, by paulson
updated for latest Blast_tac, which fixes an equality bug
1997-12-03, by paulson
Miniscoping now used except for one proof
1997-12-03, by paulson
adapted to new term order;
1997-12-02, by wenzelm
tuned term order;
1997-12-02, by wenzelm
tuned trfuns types;
1997-12-02, by wenzelm
added prod_ord, dict_ord, list_ord;
1997-12-02, by wenzelm
File.tmp_name;
1997-12-02, by wenzelm
added tmp_name;
1997-12-02, by wenzelm
ISABELLE_TMP;
1997-12-02, by wenzelm
added context.ML;
1997-12-02, by wenzelm
Global contexts: session and theory.
1997-12-02, by wenzelm
added Thy/context.ML;
1997-12-02, by wenzelm
open;
1997-12-01, by wenzelm
nat_cancel simprocs;
1997-12-01, by wenzelm
ISABELLE_TMP_PREFIX;
1997-12-01, by wenzelm
ISABELLE_TMP;
1997-12-01, by wenzelm
Added DiffCancelSums.
1997-12-01, by berghofe
New guarantee B_trusts_NS5, and tidying
1997-12-01, by paulson
speed-up
1997-12-01, by paulson
args for record data
1997-12-01, by narasche
Removed "open Mutil;"
1997-11-28, by nipkow
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
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
restored last version
1997-11-12, by oheimb
simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
1997-11-12, by oheimb
renamed split_T_case_prem to split_T_case_asm
1997-11-12, by oheimb
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
less
more
|
(0)
-3000
-1000
-256
+256
+1000
+3000
+10000
+30000
tip