Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-512
+512
+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
Fixed indentation
1997-11-11, by paulson
Rationalized the theorem if_image_distrib.
1997-11-11, by paulson
Fixed indentation
1997-11-11, by paulson
Fixed spelling error
1997-11-11, by paulson
Made some proofs more robust
1997-11-11, by paulson
Now applies "map negOfGoal" to lits when expanding haz rules.
1997-11-11, by paulson
ASCII-fied;
1997-11-10, by wenzelm
polished definition of find_index_eq
1997-11-10, by oheimb
check files for non-ASCII characters;
1997-11-10, by wenzelm
replaced 8bit characters
1997-11-10, by oheimb
fixed LAM<...> syntax;
1997-11-10, by wenzelm
fixed spelling;
1997-11-10, by wenzelm
added split_prem_tac
1997-11-07, by oheimb
changed libraray function find to find_index_eq, currying it
1997-11-07, by oheimb
added contrapos
1997-11-07, by oheimb
added contrapos2
1997-11-07, by oheimb
added exists_Const
1997-11-07, by oheimb
Each datatype t now proves a theorem split_t_case_prem
1997-11-07, by nipkow
Perl no longer optional;
1997-11-06, by wenzelm
deriv: eliminated references to theory;
1997-11-06, by wenzelm
tuned;
1997-11-06, by wenzelm
tuned;
1997-11-06, by wenzelm
hyp_subst_tac checks if the equality has type variables and uses a suitable
1997-11-06, by paulson
subgoal_tac displays a warning if the new subgoal has type variables
1997-11-06, by paulson
mkdir -p bin;
1997-11-05, by wenzelm
Tools/8bit: ./mk;
1997-11-05, by wenzelm
*** empty log message ***
1997-11-05, by oheimb
tuned;
1997-11-05, by wenzelm
abandoned generation of tmp files
1997-11-05, by oheimb
various improvements
1997-11-05, by oheimb
reflecting changes of isa2latex
1997-11-05, by oheimb
several minor improvements
1997-11-05, by oheimb
added ax2isa
1997-11-05, by oheimb
added ax2isa
1997-11-05, by oheimb
added isabelle14 and isabelle24
1997-11-05, by oheimb
removed gererated files
1997-11-05, by oheimb
added entry for manual
1997-11-05, by oheimb
*** empty log message ***
1997-11-05, by oheimb
Now introduces Safe_tac
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
Adapted to removal of UN1_I, etc
1997-11-05, by paulson
Adapted to removal of UN1_I, etc
1997-11-05, by paulson
UNIV now a constant; UNION1, INTER1 now translations and no longer have
1997-11-05, by paulson
Expandshort; new theorem le_square
1997-11-05, by paulson
generalized UNION1 to UNION
1997-11-05, by paulson
Tidied Key_supply3
1997-11-05, by paulson
fixed comment
1997-11-05, by paulson
UNIV & UNION1
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
adapted typed_print_translation;
1997-11-05, by wenzelm
tuned record_info;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
adapted pure_trfunsT;
1997-11-05, by wenzelm
print translation: added show_sorts argument;
1997-11-05, by wenzelm
adapted syn_ext_trfunsT;
1997-11-05, by wenzelm
adapted extend_trfunsT;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
added TYPE syntax;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
adapted add_trfunsT;
1997-11-05, by wenzelm
adapted add_trfunsT;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
base root = "";
1997-11-05, by wenzelm
Added an alternativ version of AutoChopper and a theory for the conversion of
1997-11-05, by nipkow
removed redundant ball_image
1997-11-04, by oheimb
removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-04, by oheimb
added several theorems
1997-11-04, by oheimb
added the, option_map, and case analysis theorems
1997-11-04, by oheimb
added zip and nodup
1997-11-04, by oheimb
added theorems for Eps
1997-11-04, by oheimb
tuned usage;
1997-11-04, by wenzelm
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
1997-11-04, by wenzelm
tuned to make non-Poly/MLs happy;
1997-11-04, by wenzelm
tuned 'records' stuff;
1997-11-04, by wenzelm
added pretty_ctyp;
1997-11-04, by wenzelm
tuned;
1997-11-04, by wenzelm
type object = exn (enhance readability);
1997-11-04, by wenzelm
*** empty log message ***
1997-11-04, by oheimb
* removed "axioms" and "generated by" section
1997-11-04, by oheimb
simplified (and corrected) syntax definition of fapp
1997-11-04, by oheimb
data kinds 'datatypes', data kinds 'records' added
1997-11-04, by narasche
removed old datatype_info;
1997-11-04, by wenzelm
added Thy/path.ML;
1997-11-04, by wenzelm
Logic.loops -> Logic.rewrite_rule_ok
1997-11-04, by nipkow
logic: loops -> rewrite_rule_ok
1997-11-04, by nipkow
added path.ML;
1997-11-04, by wenzelm
added base;
1997-11-04, by wenzelm
Abstract algebra of file paths. External representation Unix-style.
1997-11-04, by wenzelm
tuned;
1997-11-04, by wenzelm
removed old thy data stuff;
1997-11-04, by wenzelm
fixed set_current_thy pattern;
1997-11-04, by wenzelm
isatool fixclasimp;
1997-11-04, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
adapted to new datatypes thy info;
1997-11-03, by wenzelm
tuned;
1997-11-03, by wenzelm
datatypes;
1997-11-03, by wenzelm
nat datatype_info moved to Nat.thy;
1997-11-03, by wenzelm
added MLtext section;
1997-11-03, by wenzelm
added distinct_fst_string;
1997-11-03, by wenzelm
tuned: distinct_fst_string;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
export const_decls parser;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
CLASET';
1997-11-03, by wenzelm
moved cladata.ML, simpdata.ML to ROOT.ML;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
adapted to new implicit simpset;
1997-11-03, by wenzelm
added claset thy_data;
1997-11-03, by wenzelm
added simpset thy_data;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
added thy_data;
1997-11-03, by wenzelm
use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;
1997-11-03, by wenzelm
adapted to new implicit simpset;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
fixed thy dependencies;
1997-11-03, by wenzelm
aded thy_data;
1997-11-03, by wenzelm
HOL theory data.
1997-11-03, by wenzelm
added thy_data.ML;
1997-11-03, by wenzelm
new implicit simpset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
new implicit claset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
adapted to new implicit claset mechanism;
1997-11-03, by wenzelm
fix references to implicit claset and simpset;
1997-11-03, by wenzelm
do not overwrite backup files;
1997-11-03, by wenzelm
set_session renamed to add_session;
1997-11-03, by wenzelm
tuned error msg;
1997-11-03, by wenzelm
made SML/97 happy;
1997-11-03, by wenzelm
expand_option_bind -> split_option_bind
1997-11-03, by nipkow
expand_option_case -> split_option_case
1997-11-03, by nipkow
*** empty log message ***
1997-11-03, by nipkow
expand_list_case -> split_list_case
1997-11-03, by nipkow
Indexed split_t_case.
1997-11-02, by nipkow
Documented `split_t_case' thm genearted by datatype.
1997-11-02, by nipkow
Fixed comments
1997-11-01, by paulson
New treatment of overloading\!
1997-11-01, by paulson
New syntax function for types
1997-11-01, by paulson
Faster lexing
1997-11-01, by paulson
New way of referring to Basis Library
1997-11-01, by paulson
mended type constraint\!
1997-11-01, by paulson
Set.thy was too specific
1997-11-01, by paulson
New Blast_tac (and minor tidying...)
1997-11-01, by paulson
Auto update
1997-11-01, by paulson
propagate exn msg;
1997-11-01, by wenzelm
dup sections: warning instead of error;
1997-10-31, by wenzelm
Session, Context;
1997-10-31, by wenzelm
tuned;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-31, by wenzelm
*** empty log message ***
1997-10-31, by wenzelm
added str_of_sg: sg -> string;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-30, by wenzelm
tuned thy_data;
1997-10-30, by wenzelm
tuned init_data;
1997-10-30, by wenzelm
added thy_data;
1997-10-30, by wenzelm
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
1997-10-30, by wenzelm
Modified trace output routines of simplifier.
1997-10-30, by nipkow
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
PureThy.add_store_defs_i, PureThy.add_store_axioms;
1997-10-30, by wenzelm
fixed try_dest_adm;
1997-10-30, by wenzelm
added adm.ML;
1997-10-30, by wenzelm
tuned;
1997-10-30, by wenzelm
tuned simp trace;
1997-10-30, by wenzelm
*** empty log message ***
1997-10-30, by nipkow
Removed spurious blank.
1997-10-30, by nipkow
Updated proofs
1997-10-30, by nipkow
For each datatype `t' there is now a theorem `split_t_case' of the form
1997-10-30, by nipkow
fixed spaces in qed;
1997-10-29, by wenzelm
debugging concerning sort variables
1997-10-29, by oheimb
PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i, PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i;
1997-10-28, by wenzelm
PureThy.add_store_axioms;
1997-10-28, by wenzelm
fixed qed;
1997-10-28, by wenzelm
do not change global_names flag;
1997-10-28, by wenzelm
restructured -- uses PureThy storage facilities;
1997-10-28, by wenzelm
added ignored_consts, thms_containing, add_store_axioms(_i),
1997-10-28, by wenzelm
always reload .ML *and* .thy file;
1997-10-28, by wenzelm
PureThy.add_store_defs, PureThy.add_store_axioms;
1997-10-28, by wenzelm
added ancestors;
1997-10-28, by wenzelm
added name_of_thm;
1997-10-28, by wenzelm
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
1997-10-28, by wenzelm
eq_thm moved to thm.ML;
1997-10-28, by wenzelm
add_store_axioms_i;
1997-10-28, by wenzelm
Added finite_UNION/SigmaI.
1997-10-28, by nipkow
oops;
1997-10-27, by wenzelm
renamed put_* to store_*;
1997-10-27, by wenzelm
flipped global_names default;
1997-10-27, by wenzelm
do not change global_names flag;
1997-10-27, by wenzelm
Isa94-2 instead of Isa95;
1997-10-27, by wenzelm
adapted domain and ax_ops package for name spaces
1997-10-27, by oheimb
made SML/NJ happy;
1997-10-27, by wenzelm
Deleted two needless theorems
1997-10-27, by paulson
internalized some names
1997-10-25, by oheimb
corrected two comments
1997-10-25, by oheimb
Added
1997-10-24, by nipkow
oops, swap warnings;
1997-10-24, by wenzelm
record: tuned output;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
merge: default to ProtoPure.thy;
1997-10-24, by wenzelm
ProtoPure.thy etc.;
1997-10-24, by wenzelm
tuned names;
1997-10-24, by wenzelm
self_ref: check_stale;
1997-10-24, by wenzelm
eq_thm (from drule.ML);
1997-10-24, by wenzelm
added declared: T -> string -> bool;
1997-10-24, by wenzelm
Pure.thy;
1997-10-24, by wenzelm
ProtoPure.thy;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
removed add_thms_as_axms;
1997-10-24, by wenzelm
Init 'theorems' data. The Pure theories.
1997-10-24, by wenzelm
added pure_thy.ML;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
Modified comment.
1997-10-24, by nipkow
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
1997-10-24, by nipkow
HOL/Map
1997-10-24, by nipkow
Added the new theory Map.
1997-10-24, by nipkow
added record section;
1997-10-23, by wenzelm
Sign.name_of;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
improved typ parser, exported;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
hide id, stamps;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
added sort_wrt;
1997-10-23, by wenzelm
fixed prune of hidden short names;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
tuned;
1997-10-22, by wenzelm
certify: check_stale;
1997-10-22, by wenzelm
improved handling of draft signatures / theories; draft thms (and
1997-10-21, by wenzelm
sg_ref: automatic adjustment of thms of draft theories;
1997-10-21, by wenzelm
commit;
1997-10-21, by wenzelm
made Poly/ML happy, but SML/NJ unhappy;
1997-10-21, by wenzelm
typo
1997-10-21, by nipkow
Corrected alphabetical order of entries in signature.
1997-10-21, by nipkow
Fixed the index entries for "recursion, general"
1997-10-21, by paulson
Many minor speedups:
1997-10-21, by paulson
New rewrite rules image_iff
1997-10-21, by paulson
Documented `addsplits'
1997-10-20, by nipkow
make SML/NJ happy;
1997-10-20, by wenzelm
rm IOA TLA;
1997-10-20, by wenzelm
tuned types;
1997-10-20, by wenzelm
tuned sig;
1997-10-20, by wenzelm
reset global_names;
1997-10-20, by wenzelm
set global_names;
1997-10-20, by wenzelm
replaced ops by consts;
1997-10-20, by wenzelm
removed Dlist;
1997-10-20, by wenzelm
\label{simp-chap} -> chap:simplification
1997-10-20, by nipkow
fixed goal_XXX;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
tuned;
1997-10-20, by wenzelm
less
more
|
(0)
-3000
-1000
-512
+512
+1000
+3000
+10000
+30000
tip