Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-192
+192
+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.
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
more Collect laws
1999-10-13, by paulson
deleted the redundant less_imp_binomial_eq_0
1999-10-13, by paulson
choose just as an infix
1999-10-13, by paulson
simplified and generalized n_sub_lemma and n_subsets
1999-10-13, by paulson
working snapshot; more steps in Alloc
1999-10-13, by paulson
projecting/extending version of drop_prog_guarantees
1999-10-13, by paulson
new theorem set_mono
1999-10-13, by paulson
a4paper;
1999-10-12, by wenzelm
a4paper;
1999-10-12, by wenzelm
a4paper;
1999-10-12, by wenzelm
a4paper;
1999-10-12, by wenzelm
new "choose" lemmas by Florian Kammueller
1999-10-12, by paulson
improved presentation;
1999-10-11, by wenzelm
bind_thm "ccontr";
1999-10-11, by wenzelm
files: separate by " ";
1999-10-11, by wenzelm
- Documented monotonicity theorems.
1999-10-11, by berghofe
a4paper;
1999-10-11, by wenzelm
tuned packages;
1999-10-11, by wenzelm
a4paper;
1999-10-11, by wenzelm
working shapshot with "projecting" and "extending"
1999-10-11, by paulson
replaced {x. True} by UNIV to work with the new simprule, Collect_const
1999-10-11, by paulson
new default simprule Collect_const and new them Diff_insert_absorb
1999-10-11, by paulson
new thm vimage_INT; deleted redundant UN_vimage
1999-10-11, by paulson
new thm Domain_mono
1999-10-11, by paulson
new thm card_Diff_singleton; tidied
1999-10-11, by paulson
more explanations;
1999-10-09, by wenzelm
tuned presentation;
1999-10-09, by wenzelm
added structured version of the proof;
1999-10-09, by wenzelm
improved;
1999-10-09, by wenzelm
bib;
1999-10-09, by wenzelm
support bibtex;
1999-10-09, by wenzelm
check format;
1999-10-09, by wenzelm
added ISABELLE_BIBTEX;
1999-10-09, by wenzelm
removed 8bit;
1999-10-09, by wenzelm
\isakeyword: italic correction;
1999-10-08, by wenzelm
old_header: proper error message;
1999-10-08, by wenzelm
tuned presentation;
1999-10-08, by wenzelm
update from Gertrud;
1999-10-08, by wenzelm
tuned;
1999-10-08, by wenzelm
url;
1999-10-08, by wenzelm
theorem database now also indexes constants "Trueprop", "all",
1999-10-08, by wenzelm
improved;
1999-10-08, by wenzelm
removed generated index.html;
1999-10-08, by wenzelm
isatool_document;
1999-10-08, by wenzelm
make: tuned usage;
1999-10-08, by wenzelm
improved presentation;
1999-10-08, by wenzelm
include document;
1999-10-08, by wenzelm
return stored thms with proper naming in derivation;
1999-10-08, by wenzelm
improved special chars;
1999-10-08, by wenzelm
removed -c option;
1999-10-08, by wenzelm
tuned usage;
1999-10-08, by wenzelm
pass RC;
1999-10-08, by wenzelm
prepare theory session document;
1999-10-08, by wenzelm
*** empty log message ***
1999-10-08, by wenzelm
tuned;
1999-10-08, by wenzelm
cd: quiet;
1999-10-07, by wenzelm
verbatim markup tokens;
1999-10-07, by wenzelm
removed verbatim markups;
1999-10-07, by wenzelm
unset ISABELLE_SETTINGS_PRESENT;
1999-10-07, by wenzelm
Replaced update_new by update.
1999-10-07, by berghofe
Added functions for enabling and disabling derivations.
1999-10-07, by berghofe
read_idents;
1999-10-07, by wenzelm
$ISATOOL;
1999-10-07, by wenzelm
unset ISABELLE_SETTINGS_PRESENT;
1999-10-07, by wenzelm
delete Tools;
1999-10-07, by wenzelm
Documented changes to HOL/inductive and function thm_deps.
1999-10-07, by berghofe
Added file Thy/thm_deps.ML
1999-10-07, by berghofe
obsolete;
1999-10-07, by wenzelm
tuned dirname;
1999-10-07, by wenzelm
removed TeX environment hacking;
1999-10-07, by wenzelm
verbatim / verb markupup commands;
1999-10-07, by wenzelm
Present.token_source after load (better errors!?);
1999-10-07, by wenzelm
Document preparation setup;
1999-10-07, by wenzelm
Isabelle wrapper for LaTeX (and friends);
1999-10-07, by wenzelm
verbatim: no markup;
1999-10-07, by wenzelm
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
1999-10-07, by wenzelm
tex_source: Buffer.write;
1999-10-07, by wenzelm
present source *before* theory load;
1999-10-07, by wenzelm
removed write_nonempty;
1999-10-07, by wenzelm
New option -d for deleting file after use.
1999-10-07, by berghofe
New function thm_deps for visualizing dependencies of theorems.
1999-10-07, by berghofe
Added file thm_deps.
1999-10-07, by berghofe
Exported function get_info.
1999-10-07, by berghofe
ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);
1999-10-06, by wenzelm
improved presentation;
1999-10-06, by wenzelm
Isar_examples/W_correct;
1999-10-06, by wenzelm
tuned presentation;
1999-10-06, by wenzelm
tuned markup commands;
1999-10-06, by wenzelm
Latex.token;
1999-10-06, by wenzelm
improved presentation;
1999-10-06, by wenzelm
improved present_token;
1999-10-06, by wenzelm
added write_nonempty;
1999-10-06, by wenzelm
fixed naming of single axioms;
1999-10-06, by wenzelm
accomodate markup commands;
1999-10-06, by wenzelm
tuned comment;
1999-10-06, by wenzelm
added markup_command;
1999-10-06, by wenzelm
OuterSyntax.markup_command;
1999-10-06, by wenzelm
improved presentation;
1999-10-06, by wenzelm
added document;
1999-10-05, by wenzelm
simplified;
1999-10-05, by wenzelm
strip_blanks;
1999-10-05, by wenzelm
got rid of most;
1999-10-05, by wenzelm
rep_datatype now stores theorems properly.
1999-10-05, by berghofe
fixed title;
1999-10-05, by wenzelm
added document;
1999-10-05, by wenzelm
tuned comments;
1999-10-05, by wenzelm
tuned comment;
1999-10-05, by wenzelm
fixed ml_store_thm(s): deriv;
1999-10-05, by wenzelm
document preparation options: -c -d;
1999-10-05, by wenzelm
conditional url/hyperref setup;
1999-10-05, by wenzelm
present token source;
1999-10-05, by wenzelm
replace add_title by add_header;
1999-10-05, by wenzelm
clear_undo replaced by clear_undos;
1999-10-05, by wenzelm
added is_toplevel;
1999-10-05, by wenzelm
clear: int argument;
1999-10-05, by wenzelm
use_dir: doc;
1999-10-05, by wenzelm
replaced clear_undo by clear_undos;
1999-10-05, by wenzelm
outer_lex.ML loaded in Thy;
1999-10-05, by wenzelm
include browser_info stuff;
1999-10-05, by wenzelm
Simple LaTeX presentation primitives (based on outer lexical syntax).
1999-10-05, by wenzelm
begin_index: document;
1999-10-05, by wenzelm
moved stuff to present.ML;
1999-10-05, by wenzelm
added Thy/latex.ML;
1999-10-05, by wenzelm
Got rid of readtm.
1999-10-05, by berghofe
Tuned inductive definition.
1999-10-05, by berghofe
updated;
1999-10-05, by wenzelm
added Thy/latex.ML;
1999-10-05, by wenzelm
Present.setup;
1999-10-05, by wenzelm
Added attribute rulify_prems (useful for modifying premises of introduction
1999-10-05, by berghofe
added copy_all;
1999-10-05, by wenzelm
clear: int arg;
1999-10-05, by wenzelm
added position;
1999-10-05, by wenzelm
Additional rules for inductive package.
1999-10-05, by berghofe
added untabify;
1999-10-05, by wenzelm
Rule not_not is now stored in theory (needed by Inductive).
1999-10-05, by berghofe
Monotonicity rules for inductive definitions can now be added to a theory via
1999-10-05, by berghofe
macros for Isabelle generated LaTeX output;
1999-10-05, by wenzelm
arithmetic now in IntArith;
1999-10-04, by wenzelm
simprocs now in IntArith;
1999-10-04, by wenzelm
IntArith;
1999-10-04, by wenzelm
Tools/typedef_package.ML;
1999-10-04, by wenzelm
eliminated ap/app;
1999-10-04, by wenzelm
proper dependencies of all theories and packages;
1999-10-04, by wenzelm
removed DatatypePackage.setup;
1999-10-04, by wenzelm
load / setup recdef package (TFL);
1999-10-04, by wenzelm
load / setup datatype package;
1999-10-04, by wenzelm
removed TFL/sys.sml;
1999-10-04, by wenzelm
obsolete;
1999-10-04, by wenzelm
renamed 'prefix' to 'prfx' (avoids clash with infix);
1999-10-04, by wenzelm
tuned;
1999-10-04, by wenzelm
mk_frees, assume_read moved here;
1999-10-04, by wenzelm
tryres, gen_make_elim moved here;
1999-10-04, by wenzelm
FOLogic.mk_conj;
1999-10-04, by wenzelm
added mk_conj, mk_disj, mk_imp;
1999-10-04, by wenzelm
added BVC;
1999-10-04, by wenzelm
added mk_conj, mk_disj, mk_imp;
1999-10-04, by wenzelm
working snapshot (even Alloc)
1999-10-04, by paulson
most results now refer to those for "extend"
1999-10-04, by paulson
fixed lookup_theory;
1999-10-04, by wenzelm
fixed CHANGED_GOAL, which is used by stac
1999-10-04, by paulson
improved theory_source presentation (hook);
1999-10-03, by wenzelm
improved theory_source presentation;
1999-10-03, by wenzelm
export token_source;
1999-10-03, by wenzelm
added Space, Comment token kinds (keep actual text);
1999-10-03, by wenzelm
fixed no_qed;
1999-10-01, by wenzelm
added Isar/obtain.ML;
1999-10-01, by wenzelm
improved 'fix' / Skolem interfaces;
1999-10-01, by wenzelm
added 'obtain' command;
1999-10-01, by wenzelm
tuned comment;
1999-10-01, by wenzelm
added prf_asm_goal;
1999-10-01, by wenzelm
added atomic_thesis;
1999-10-01, by wenzelm
The 'obtain' language element -- achieves (eliminated) existential
1999-10-01, by wenzelm
added undef_global_attribute, undef_local_attribute;
1999-10-01, by wenzelm
- Fixed bug in mk_split_pack which caused application of expansion theorem
1999-10-01, by berghofe
fixed 'is' match;
1999-09-30, by wenzelm
added cert_skolem;
1999-09-30, by wenzelm
export find_free;
1999-09-30, by wenzelm
removed ProofContext.declare_thm;
1999-09-30, by wenzelm
local_def_i: typ option;
1999-09-30, by wenzelm
fix_i, local_def_i: typ option;
1999-09-30, by wenzelm
get_goal: prop;
1999-09-30, by wenzelm
insert: ignore facts;
1999-09-30, by wenzelm
export def_sort, def_type;
1999-09-30, by wenzelm
Real/HahnBanach;
1999-09-30, by wenzelm
depend on Main;
1999-09-30, by wenzelm
now with (weak safety) guarantees (weak progress) with Extend
1999-09-30, by paulson
bind_thm ("case_split", case_split_thm);
1999-09-29, by wenzelm
CollectE;
1999-09-29, by wenzelm
less
more
|
(0)
-3000
-1000
-192
+192
+1000
+3000
+10000
+30000
tip