Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-480
+480
+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.
fixed WWW links
1998-02-02, by paulson
Three new facts about Image
1998-02-02, by paulson
Replaced \\1 by $1 as Perl itself asked me to...
1998-02-02, by paulson
Fixed the description of recdef
1998-01-30, by paulson
tuned msgs;
1998-01-30, by wenzelm
improved tracing of rewrite rule application;
1998-01-30, by wenzelm
removed dead messy code;
1998-01-30, by wenzelm
added read_var;
1998-01-30, by wenzelm
tuned;
1998-01-30, by wenzelm
Updated MOD reference
1998-01-23, by paulson
added symbols syntax;
1998-01-21, by wenzelm
reorganized into individual theories;
1998-01-20, by wenzelm
tuned;
1998-01-19, by wenzelm
make images;
1998-01-19, by wenzelm
tuned URL;
1998-01-15, by wenzelm
polyml-3.1;
1998-01-15, by wenzelm
obsolete;
1998-01-15, by wenzelm
added thms wrt weakening and strengthening in Abstraction;
1998-01-14, by mueller
New Jersey inactive;
Isabelle98
1998-01-14, by wenzelm
HOL/record;
1998-01-14, by wenzelm
error with instantiantion of sub-records removed
1998-01-14, by narasche
added record.ML;
1998-01-14, by wenzelm
tuned;
1998-01-14, by wenzelm
added unit and prod stuff;
1998-01-14, by wenzelm
fixed Id;
1998-01-14, by wenzelm
smlnj-110 factory default;
1998-01-14, by wenzelm
added of_sort;
1998-01-14, by wenzelm
added base_path;
1998-01-13, by wenzelm
added simulations files to IOA;
1998-01-13, by mueller
added forward simulation correectness;
1998-01-13, by mueller
Simplification: sel make and update make
1998-01-13, by narasche
added abstraction files;
1998-01-12, by mueller
added further IOA liles;
1998-01-12, by mueller
updated to Isabelle98;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
added files containing temproal logic and abstraction;
1998-01-12, by mueller
Delsimprocs nat_cancel;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
1998-01-12, by paulson
tuned;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
fixed author;
1998-01-12, by wenzelm
Simplified proofs by omitting PA = {|XA, ...|} from RA2
1998-01-10, by paulson
trivial tidy
1998-01-10, by paulson
tuned;
1998-01-09, by wenzelm
automatic index.html patch;
1998-01-09, by wenzelm
tuned;
1998-01-09, by wenzelm
tuned ISABELLE_TMP_PREFIX;
1998-01-09, by wenzelm
thm_ord;
1998-01-09, by wenzelm
eliminated make_ord;
1998-01-09, by wenzelm
ISABELLE_TMP_PREFIX: $LOGNAME
1998-01-09, by wenzelm
several minor updates;
1998-01-09, by wenzelm
tuned;
1998-01-08, by wenzelm
index.html for Isabelle Distribution Area;
1998-01-08, by wenzelm
updated to Isabelle98;
1998-01-08, by wenzelm
tuned;
1998-01-08, by wenzelm
fixed thm_less;
1998-01-08, by wenzelm
Expressed most Oops rules using Notes instead of Says, and other tidying
1998-01-08, by paulson
added split_paired_Ex to the implicit simpset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added newline at end of file
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by oheimb
streamlined specification of included theories
1998-01-08, by oheimb
corrected Title
1998-01-08, by oheimb
removed obsolete comment
1998-01-08, by oheimb
added Univalent
1998-01-08, by oheimb
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
1998-01-08, by oheimb
added update_same, update_other, update_triv, and map_of_SomeD
1998-01-08, by oheimb
replaced fn _ => by K
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by wenzelm
New rule: image_subset
1998-01-08, by paulson
Restored the ciphertext in OR4 in order to make the spec closer to that in
1998-01-08, by paulson
Tidied by adding more default simprules
1998-01-08, by paulson
adapted to new split order;
1998-01-07, by wenzelm
adapted to new sort function;
1998-01-07, by wenzelm
improved targets;
1998-01-07, by wenzelm
tuned;
1998-01-06, by wenzelm
added -u option (again);
1998-01-05, by wenzelm
Now calls Blast_tac more often
1998-01-05, by paulson
obsolete;
1998-01-02, by wenzelm
feeder;
1998-01-02, by wenzelm
Changed required by new blast_tac (the one that squashes flex-flex pairs)
1998-01-02, by paulson
Blast_tac now squashes flex-flex pairs immediately
1998-01-02, by paulson
New theorem image_subsetI
1998-01-02, by paulson
Making proofs faster, especially using keysFor_parts_insert
1998-01-02, by paulson
do require perl;
1998-01-02, by wenzelm
Auto_tac now has type tactic, not unit->tactic
1998-01-02, by paulson
Declared startTiming and endTiming
1998-01-02, by paulson
use feeder to pipe into ML;
1997-12-31, by wenzelm
removed -i option;
1997-12-31, by wenzelm
nth -> !
1997-12-30, by nipkow
nth -> !
1997-12-30, by nipkow
feed isabelle session;
1997-12-29, by wenzelm
commented out symboloutput.pl;
1997-12-29, by wenzelm
added feeder.pl;
1997-12-29, by wenzelm
pretty_name_space;
1997-12-29, by wenzelm
removed declared;
1997-12-29, by wenzelm
removed distinct_fst_string;
1997-12-29, by wenzelm
improved error handling;
1997-12-28, by wenzelm
fixed execute;
1997-12-28, by wenzelm
made MLWorks happy;
1997-12-28, by wenzelm
stderr to $LOG;
1997-12-28, by wenzelm
Symtab.empty;
1997-12-28, by wenzelm
improved internal representation;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
added >> : (theory -> theory) -> unit;
1997-12-28, by wenzelm
tuned;
1997-12-28, by wenzelm
replaced symtab.ML by table.ML;
1997-12-28, by wenzelm
renamed (is_)null to (is_)empty;
1997-12-28, by wenzelm
Generic tables (lacking delete operation). Implemented as 2-3 trees.
1997-12-27, by wenzelm
tuned;
1997-12-24, by wenzelm
export range_type;
1997-12-24, by wenzelm
improved comment;
1997-12-24, by wenzelm
More restrictive patterns to prevent changing comments
1997-12-24, by paulson
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-24, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Now Blast_tac works properly
1997-12-23, by paulson
Tidied. Also better proof using new blast_tac
1997-12-23, by paulson
Decremented subscript because of change to iffD1
1997-12-23, by paulson
Tidied using rev_iffD1, etc
1997-12-23, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Tidied using more default rules
1997-12-23, by paulson
Overloading info for image
1997-12-23, by paulson
tidied
1997-12-23, by paulson
New rules rev_iffD{1,2}
1997-12-23, by paulson
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-23, by paulson
New "obvious theorems"
1997-12-23, by paulson
Added range-type for completeness
1997-12-22, by paulson
New example
1997-12-22, by paulson
New rules rev_iffD{1,2}
1997-12-22, by paulson
corrected removal to /tmp/tmp.c
1997-12-19, by oheimb
added removal to /tmp/tmp.txt
1997-12-19, by oheimb
records without signature
1997-12-19, by narasche
remove signatrue from records
1997-12-19, by narasche
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
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip