Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-112
+112
+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.
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
subsetD;
1999-09-29, by wenzelm
update from Gertrud;
1999-09-29, by wenzelm
The Hahn-Banach theorem for real vectorspaces;
1999-09-29, by wenzelm
bind_thms;
1999-09-29, by wenzelm
Sign.defaultS;
1999-09-29, by wenzelm
Sign.of_sort;
1999-09-29, by wenzelm
tuned;
1999-09-29, by wenzelm
removed force_strip_shyps;
1999-09-29, by wenzelm
lemma;
1999-09-29, by wenzelm
bind_thms;
1999-09-29, by wenzelm
proper handling of dangling sort hypotheses (at last!);
1999-09-29, by wenzelm
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
1999-09-29, by wenzelm
Sign.defaultS;
1999-09-29, by wenzelm
strip_shyps(_warning);
1999-09-29, by wenzelm
mg_domain: exception DOMAIN;
1999-09-29, by wenzelm
removed implies_intr_shyps;
1999-09-29, by wenzelm
added witness_sorts, univ_witness;
1999-09-29, by wenzelm
added witness_sorts, univ_witness;
1999-09-29, by wenzelm
handle Sorts.DOMAIN;
1999-09-29, by wenzelm
added rems_sort;
1999-09-29, by wenzelm
use Drule.strip_shyps_warning;
1999-09-29, by wenzelm
strip_shyps_warning;
1999-09-29, by wenzelm
new tsig components;
1999-09-29, by wenzelm
more sections;
1999-09-29, by wenzelm
present sections;
1999-09-29, by wenzelm
removed extra shyps error;
1999-09-29, by wenzelm
added string_of: text -> string;
1999-09-29, by wenzelm
working snapshot with new theory "Project"
1999-09-29, by paulson
tuned;
1999-09-28, by wenzelm
tidied, using "warning" function and fixing the Close_locale bug
1999-09-28, by paulson
added BCV.
1999-09-28, by nipkow
A new theory: a model of bytecode verification.
1999-09-28, by nipkow
zero_is_mult, by symmetry
1999-09-28, by paulson
new UNITY theory: Project
1999-09-28, by paulson
AC rules for equality
1999-09-28, by paulson
zero_is_mult, by symmetry
1999-09-28, by paulson
added W_correct -- correctness of Milner's type inference algorithm W
1999-09-28, by wenzelm
documented type solver
1999-09-28, by nipkow
incompatibility solver
1999-09-28, by nipkow
more tidying
1999-09-28, by paulson
removed order-sorted theorems from the default claset
1999-09-27, by paulson
added 'thms_containing', 'ML_setup';
1999-09-26, by wenzelm
added print_thms_containing;
1999-09-26, by wenzelm
use_mltext: Context.setmp only;
1999-09-26, by wenzelm
help: unknown theory context;
1999-09-26, by wenzelm
added keep', theory';
1999-09-26, by wenzelm
help: unkown theory context;
1999-09-26, by wenzelm
less
more
|
(0)
-3000
-1000
-112
+112
+1000
+3000
+10000
+30000
tip