Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-240
+240
+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.
new arg type for max_spec etc.
2000-01-04, by oheimb
small changes;
2000-01-03, by bauerg
removed inj_eq from the default simpset again
2000-01-03, by oheimb
removed inj_eq from the default simpset again
2000-01-03, by oheimb
removed inj_eq from the default simpset again
1999-12-23, by oheimb
updated sml package name in installation exmaple
1999-12-23, by kleing
raw_t(e)xt: any proof mode;
1999-12-22, by wenzelm
fixed error msg;
1999-12-22, by wenzelm
marg_comment: repeat;
1999-12-22, by wenzelm
text: string list;
1999-12-22, by wenzelm
tidied, with a bit more progress
1999-12-22, by paulson
Working version after a FAILED attempt to base Follows upon LeadsETo
1999-12-22, by paulson
new weakening laws
1999-12-22, by paulson
removing the "{} : CC" requirement for leadsTo[CC]
1999-12-22, by paulson
back to old sml version (due to c library problems)
1999-12-22, by kleing
some tuning (incorporated David's suggestions)
1999-12-22, by kleing
working with weak LeadsTo in guarantees precondition\!
1999-12-21, by paulson
corrected, improved eMail addresses, user interface section
1999-12-21, by oheimb
now workign as far as System_Alloc_Progress
1999-12-17, by paulson
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
1999-12-16, by paulson
first working version to Alloc/System_Client_Progress;
1999-12-15, by paulson
expandshort
1999-12-13, by paulson
dist page now in page/dist-{content|layout}
1999-12-09, by kleing
updated;
1999-12-09, by wenzelm
prettyfied
1999-12-09, by kleing
full url to local (munich) page
1999-12-09, by kleing
new web pages integrated
1999-12-09, by kleing
used for new weg page layout
1999-12-09, by kleing
ID line added
1999-12-09, by kleing
new webpage layout
1999-12-09, by kleing
abolition of localTo: instead "guarantees" has local vars as extra argument
1999-12-08, by paulson
used image_eq_UN to speed up slow proofs of base cases
1999-12-08, by paulson
useful lemma eqset_imp_iff
1999-12-08, by paulson
tuned;
1999-12-07, by wenzelm
tuned;
1999-12-07, by wenzelm
added Isar_examples/Fibonacci.thy;
1999-12-07, by wenzelm
Fixed bug in find-functions: list of parameters must be reversed before
1999-12-07, by nipkow
Renamed some vars
1999-12-06, by nipkow
cosmetic mod.
1999-12-02, by nipkow
accommodate current version of rpm;
1999-12-01, by wenzelm
Fixed a problem with returning from the last frame.
1999-12-01, by nipkow
new generalized leads-to theory
1999-12-01, by paulson
fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER
1999-12-01, by paulson
deleted rogue copy of localTo_imp_o_localTo
1999-11-30, by paulson
working version with new theory ELT
1999-11-30, by paulson
new theory UNITY/ELT
1999-11-30, by paulson
Goal: tuned pris;
1999-11-29, by wenzelm
Removed !!
1999-11-29, by nipkow
Minimal.thy;
1999-11-29, by wenzelm
Isar_examples/Minimal.thy;
1999-11-29, by wenzelm
qed "";
1999-11-29, by wenzelm
Various little changes like cmethd -> method and cfield -> field.
1999-11-26, by nipkow
del Method.ML
1999-11-25, by nipkow
Minor mods.
1999-11-25, by nipkow
renamed comp to compile (avoids clash with Relation.comp);
1999-11-24, by wenzelm
prove_goal thy;
1999-11-24, by wenzelm
Basis now Main.
1999-11-24, by nipkow
tidied, choosing nicer names
1999-11-24, by paulson
distributive laws for * over -
1999-11-23, by paulson
tidied
1999-11-23, by paulson
new theorem rev_image_eqI
1999-11-23, by paulson
Added linord_less_split
1999-11-22, by nipkow
re-shaped and re-ordered conversion relations
1999-11-19, by oheimb
Streamlined it a bit more.
1999-11-18, by nipkow
A small mod.
1999-11-18, by nipkow
added Isar_examples/Puzzle.thy;
1999-11-17, by wenzelm
tidied
1999-11-17, by paulson
Streamlined it a bit.
1999-11-15, by nipkow
removed full_SetCompr_eq from simpset() again
1999-11-12, by oheimb
Added the proof by Nielson & Nielson.
1999-11-12, by nipkow
tuned;
1999-11-12, by wenzelm
HOL changes
1999-11-11, by paulson
*** empty log message ***
1999-11-11, by nipkow
Added MicroJava
1999-11-11, by nipkow
*** empty log message ***
1999-11-11, by nipkow
with_path;
1999-11-11, by wenzelm
Imported Conny's lemmas from MicroJava
1999-11-11, by nipkow
clean target;
1999-11-11, by wenzelm
header;
1999-11-11, by wenzelm
tidied
1999-11-11, by paulson
new-style infix declaration for "image"
1999-11-11, by paulson
Fixed obsolete use of "op ^^"; new lemma
1999-11-11, by paulson
tuned;
1999-11-06, by wenzelm
tidied
1999-11-05, by paulson
new psubset lemma
1999-11-05, by paulson
added foldr
1999-11-05, by paulson
Algebra and Polynomial theories, by Clemens Ballarin
1999-11-05, by paulson
Algebra and Polynomial theories, by Clemens Ballarin
1999-11-05, by paulson
tuned;
1999-11-03, by wenzelm
MUCKE_HOME;
1999-11-03, by wenzelm
Id;
1999-11-03, by wenzelm
improved;
1999-11-03, by wenzelm
tuned;
1999-11-02, by wenzelm
RPMRELEASE;
1999-11-01, by wenzelm
inserted {...}
1999-11-01, by paulson
updated;
Isabelle99
1999-10-31, by wenzelm
updated;
1999-10-31, by wenzelm
tuned;
1999-10-31, by wenzelm
tuned;
1999-10-31, by wenzelm
Isabelle99;
1999-10-30, by wenzelm
fixed deps;
1999-10-30, by wenzelm
tuned;
1999-10-30, by wenzelm
tuned;
1999-10-30, by wenzelm
improved presentation;
1999-10-30, by wenzelm
tuned;
1999-10-30, by wenzelm
isabellesym.sty;
1999-10-30, by wenzelm
definitions of many Isabelle symbols;
1999-10-30, by wenzelm
final update by Gertrud Bauer;
1999-10-29, by wenzelm
workaround bug (feature?) in bibtex;
1999-10-29, by wenzelm
tuned;
1999-10-29, by wenzelm
comment out isabellesym.sty;
1999-10-29, by wenzelm
improved;
1999-10-29, by wenzelm
\isasymbol renamed to \isasym;
1999-10-29, by wenzelm
tuned;
1999-10-29, by wenzelm
tuned msg;
1999-10-29, by wenzelm
\isasym;
1999-10-29, by wenzelm
improved singleton_insert_inj_eq
1999-10-29, by oheimb
improved presentation;
1999-10-28, by wenzelm
fixed deps;
1999-10-28, by wenzelm
tuned;
1999-10-28, by wenzelm
expandshort; tidied
1999-10-28, by paulson
localTo_imp_o_localTo is now really an implication
1999-10-28, by paulson
simplified the stable_completion proofs
1999-10-28, by paulson
tidied
1999-10-28, by paulson
expandshort
1999-10-28, by paulson
improved IsarThy.init_context;
1999-10-28, by wenzelm
tuned;
1999-10-28, by wenzelm
added various little lemmas
1999-10-27, by oheimb
clarsimp_tac now copes with the (unwanted) case that the simplifier splits
1999-10-27, by oheimb
tuned msg;
1999-10-27, by wenzelm
tuned;
1999-10-27, by wenzelm
added (try_)update_thy_only;
1999-10-27, by wenzelm
added init_context;
1999-10-27, by wenzelm
quiet_update_thy: ml flag;
1999-10-27, by wenzelm
Fixed a bug in the EX simproc.
1999-10-27, by nipkow
export cond_with_path;
1999-10-27, by wenzelm
dummy_pattern: aprop;
1999-10-27, by wenzelm
updated for Isabelle99;
1999-10-27, by wenzelm
working again; new treatment of LocalTo
1999-10-27, by paulson
TEMPORARY use of Addsimps
1999-10-27, by paulson
got rid of split_diff, which duplicated nat_diff_split, and
1999-10-27, by paulson
symbols in (error) messages now consistently with single backslash
1999-10-27, by oheimb
now more than 256 generated bound variables possible
1999-10-27, by oheimb
reset_goals no longer empties the proof stack
1999-10-27, by oheimb
improved ml handling;
1999-10-26, by wenzelm
improved ml handling;
1999-10-26, by wenzelm
tuned;
1999-10-26, by wenzelm
activate ml_prompts;
1999-10-26, by wenzelm
added inform_file_processed, inform_file_retracted;
1999-10-26, by wenzelm
added kill_proof_notify;
1999-10-26, by wenzelm
added check_known_thy, if_known_thy;
1999-10-26, by wenzelm
Isabelle %f;
1999-10-26, by wenzelm
do not set proof_timing;
1999-10-26, by wenzelm
export kill_theory;
1999-10-26, by wenzelm
added kill_thy;
1999-10-26, by wenzelm
added opt_unit (from isar_syn.ML);
1999-10-26, by wenzelm
added drop_ext;
1999-10-26, by wenzelm
improved handling of warn_extra_tfrees;
1999-10-25, by wenzelm
update by Gertrud Bauer;
1999-10-25, by wenzelm
added Real/HahnBanach/document/root.bib;
1999-10-25, by wenzelm
warn_extra_tfrees (after declare_term);
1999-10-22, by wenzelm
warn_extra_tfrees;
1999-10-22, by wenzelm
warn_extra_tfrees;
1999-10-22, by wenzelm
tuned repeat_undo;
1999-10-22, by wenzelm
debug_simp;
1999-10-22, by wenzelm
new flag debug_simp
1999-10-22, by wenzelm
tuned simplifier trace output; new flag debug_simp
1999-10-22, by wenzelm
achieve proper italic correction;
1999-10-22, by wenzelm
HahnBanach update by Gertrud Bauer;
1999-10-22, by wenzelm
replaced image_image_eq_UN by image_eq_UN
1999-10-22, by paulson
ALMOST working version: LocalTo results commented out
1999-10-22, by paulson
new default simprules for UN and INT
1999-10-22, by paulson
new theorems on Image
1999-10-22, by paulson
tidied using modern infix form
1999-10-22, by paulson
tuned trace_action;
1999-10-21, by wenzelm
added known_thy;
1999-10-21, by wenzelm
end/kill_theory: check_known_thy;
1999-10-21, by wenzelm
added touch_child_thys;
1999-10-21, by wenzelm
\isakeyword: fixed italic correction;
1999-10-21, by wenzelm
get_thm;
1999-10-21, by wenzelm
tuned;
1999-10-21, by wenzelm
proper handling of axioms / defs;
1999-10-21, by wenzelm
markup: keep indentation;
1999-10-21, by wenzelm
added is_indent;
1999-10-21, by wenzelm
export thy_path;
1999-10-21, by wenzelm
output \isasymbols;
1999-10-21, by wenzelm
forall_elim_var(s) move here from drule.ML;
1999-10-21, by wenzelm
forall_elim_var(s) moved to pure_thy.ML;
1999-10-21, by wenzelm
*** empty log message ***
1999-10-21, by wenzelm
removed \BG, \EN;
1999-10-21, by wenzelm
updated;
1999-10-21, by wenzelm
added \ISS;
1999-10-21, by wenzelm
eliminated isar_action;
1999-10-20, by wenzelm
remove_thy: warn unknown theory (rather than error);
1999-10-20, by wenzelm
use_mltext: better control of verbosity;
1999-10-20, by wenzelm
use_text: remove last char from output;
1999-10-20, by wenzelm
option -m TARGET;
1999-10-20, by wenzelm
removed -B option;
1999-10-20, by wenzelm
tuned usage;
1999-10-20, by wenzelm
the settings environment is now statically scoped;
1999-10-20, by wenzelm
fixed update_thy_only;
1999-10-20, by wenzelm
qed_spec_mp is a mess;
1999-10-19, by wenzelm
tuned;
1999-10-19, by wenzelm
tuned;
1999-10-18, by wenzelm
update by Stephan Merz;
1999-10-18, by wenzelm
exchanged the first two args of "project" and "drop_prog"
1999-10-18, by paulson
fixed comments
1999-10-18, by paulson
working version with localTo[C] instead of localTo
1999-10-18, by paulson
new thm disjoint_iff_not_equal
1999-10-18, by paulson
new thm vimage_image_eq
1999-10-18, by paulson
PROOFGENERAL_OPTIONS="-u false";
1999-10-16, by wenzelm
improved presentation;
1999-10-15, by wenzelm
fixed comment;
1999-10-15, by wenzelm
Removed obsolete comment.
1999-10-15, by berghofe
Documented thm_deps.
1999-10-15, by berghofe
Corrected typo.
1999-10-14, by berghofe
improved presentation;
1999-10-14, by wenzelm
support thumbpdf;
1999-10-14, by wenzelm
fixed comment;
1999-10-14, by wenzelm
pdf: generate thumbnails if ISABELLE_THUMBPDF set;
1999-10-14, by wenzelm
support thumbpdf (via 'png' output format);
1999-10-14, by wenzelm
thumbpdf (disabled by default);
1999-10-14, by wenzelm
document preparation based on (PDF)LaTeX;
1999-10-14, by wenzelm
renamed verbatim/verb to text_raw/txt_raw;
1999-10-14, by wenzelm
tuned;
1999-10-14, by wenzelm
improved presentation;
1999-10-14, by wenzelm
berghofe;
1999-10-13, by wenzelm
isabelle-isar-ref;
1999-10-13, by wenzelm
tuned usage;
1999-10-13, by wenzelm
-d pdf;
1999-10-13, by wenzelm
system;
1999-10-13, by wenzelm
use_text_verbose;
1999-10-13, by wenzelm
system;
1999-10-13, by wenzelm
markup / varbatim: comment out (%) newline char;
1999-10-13, by wenzelm
use_text writeln;
1999-10-13, by wenzelm
mkdir, copy_all: system_command;
1999-10-13, by wenzelm
updated;
1999-10-13, by wenzelm
Eliminated mutual_induct_tac.
1999-10-13, by berghofe
Eliminated mutual_induct_tac.
1999-10-13, by berghofe
Eliminated mutual_induct_tac.
1999-10-13, by berghofe
less
more
|
(0)
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip