| 2013-05-25 |
wenzelm |
2013-05-25 |
syntax translations always depend on context;
|
file | diff | annotate |
| 2012-11-16 |
hoelzl |
2012-11-16 |
moved (b)choice_iff(') to Hilbert_Choice
|
file | diff | annotate |
| 2012-10-20 |
haftmann |
2012-10-20 |
moved quite generic material from theory Enum to more appropriate places
|
file | diff | annotate |
| 2012-10-08 |
haftmann |
2012-10-08 |
consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common
|
file | diff | annotate |
| 2012-08-22 |
wenzelm |
2012-08-22 |
prefer ML_file over old uses;
|
file | diff | annotate |
| 2012-05-24 |
wenzelm |
2012-05-24 |
tuned proofs;
|
file | diff | annotate |
| 2012-03-15 |
wenzelm |
2012-03-15 |
declare command keywords via theory header, including strict checking outside Pure;
|
file | diff | annotate |
| 2011-11-20 |
wenzelm |
2011-11-20 |
eliminated obsolete "standard";
|
file | diff | annotate |
| 2011-09-13 |
huffman |
2011-09-13 |
tuned proofs
|
file | diff | annotate |
| 2011-09-12 |
nipkow |
2011-09-12 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
|
file | diff | annotate |
| 2010-11-23 |
hoelzl |
2010-11-23 |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file | diff | annotate |
| 2010-11-22 |
hoelzl |
2010-11-22 |
Replace surj by abbreviation; remove surj_on.
|
file | diff | annotate |
| 2010-10-05 |
blanchet |
2010-10-05 |
got rid of overkill "meson_choice" attribute;
tuning
|
file | diff | annotate |
| 2010-10-04 |
blanchet |
2010-10-04 |
remove Meson from Hilbert_Choice
|
file | diff | annotate |
| 2010-10-01 |
blanchet |
2010-10-01 |
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-09-02 |
blanchet |
2010-09-02 |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine
|
file | diff | annotate |
| 2010-03-01 |
haftmann |
2010-03-01 |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file | diff | annotate |
| 2010-02-18 |
huffman |
2010-02-18 |
get rid of many duplicate simp rule warnings
|
file | diff | annotate |
| 2010-02-11 |
wenzelm |
2010-02-11 |
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
|
file | diff | annotate |
| 2009-10-22 |
nipkow |
2009-10-22 |
inv_onto -> inv_into
|
file | diff | annotate |
| 2009-10-20 |
nipkow |
2009-10-20 |
added inv_def for compatibility as a lemma
|
file | diff | annotate |
| 2009-10-18 |
nipkow |
2009-10-18 |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
file | diff | annotate |
| 2009-06-19 |
haftmann |
2009-06-19 |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file | diff | annotate |
| 2009-06-04 |
haftmann |
2009-06-04 |
dropped legacy ML bindings; tuned
|
file | diff | annotate |
| 2009-06-02 |
haftmann |
2009-06-02 |
added/moved lemmas by Andreas Lochbihler
|
file | diff | annotate |
| 2009-01-28 |
haftmann |
2009-01-28 |
Plain, Main form meeting points in import hierarchy
|
file | diff | annotate |
| 2008-08-06 |
nipkow |
2008-08-06 |
added lemma
|
file | diff | annotate |
| 2008-04-25 |
krauss |
2008-04-25 |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file | diff | annotate |
| 2008-04-07 |
paulson |
2008-04-07 |
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
|
file | diff | annotate |
| 2008-03-20 |
haftmann |
2008-03-20 |
tuned proofs
|
file | diff | annotate |
| 2008-02-21 |
nipkow |
2008-02-21 |
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
added some
|
file | diff | annotate |
| 2008-02-15 |
haftmann |
2008-02-15 |
<= and < on nat no longer depend on wellfounded relations
|
file | diff | annotate |
| 2007-06-20 |
nipkow |
2007-06-20 |
added lemmas
|
file | diff | annotate |
| 2007-04-15 |
wenzelm |
2007-04-15 |
replaced axioms/finalconsts by proper axiomatization;
|
file | diff | annotate |
| 2007-01-04 |
paulson |
2007-01-04 |
improvements to proof reconstruction. Some files loaded in a different order
|
file | diff | annotate |
| 2006-11-08 |
wenzelm |
2006-11-08 |
removed theory NatArith (now part of Nat);
|
file | diff | annotate |
| 2006-10-13 |
berghofe |
2006-10-13 |
Adapted to changes in FixedPoint theory.
|
file | diff | annotate |
| 2005-12-13 |
paulson |
2005-12-13 |
removal of functional reflexivity axioms
|
file | diff | annotate |
| 2005-10-18 |
wenzelm |
2005-10-18 |
added lemma exE_some (from specification_package.ML);
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
more finalconsts;
|
file | diff | annotate |
| 2005-09-15 |
paulson |
2005-09-15 |
comment
|
file | diff | annotate |
| 2005-07-13 |
paulson |
2005-07-13 |
generlization of some "nat" theorems
|
file | diff | annotate |
| 2005-06-24 |
paulson |
2005-06-24 |
meson method taking an argument list
|
file | diff | annotate |
| 2005-06-17 |
haftmann |
2005-06-17 |
migrated theory headers to new format
|
file | diff | annotate |
| 2004-10-19 |
paulson |
2004-10-19 |
converted some induct_tac to induct
|
file | diff | annotate |
| 2004-08-18 |
nipkow |
2004-08-18 |
import -> imports
|
file | diff | annotate |
| 2004-08-16 |
nipkow |
2004-08-16 |
New theory header syntax.
|
file | diff | annotate |
| 2004-06-05 |
wenzelm |
2004-06-05 |
improved symbolic syntax of Eps: \<some> for mode "epsilon";
|
file | diff | annotate |
| 2004-05-19 |
paulson |
2004-05-19 |
conversion of Hilbert_Choice to Isar script
|
file | diff | annotate |
| 2004-02-19 |
ballarin |
2004-02-19 |
New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.
|
file | diff | annotate |
| 2003-09-26 |
paulson |
2003-09-26 |
misc tidying
|
file | diff | annotate |
| 2003-07-17 |
skalberg |
2003-07-17 |
Added package for definition by specification.
|
file | diff | annotate |
| 2002-12-22 |
nipkow |
2002-12-22 |
removed some problems with print translations
|
file | diff | annotate |
| 2002-12-22 |
nipkow |
2002-12-22 |
added print translations tha avoid eta contraction for important binders.
|
file | diff | annotate |
| 2002-09-26 |
paulson |
2002-09-26 |
Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"
|
file | diff | annotate |
| 2001-12-05 |
wenzelm |
2001-12-05 |
tuned declarations;
|
file | diff | annotate |
| 2001-11-26 |
wenzelm |
2001-11-26 |
tuned;
meson lemmas from Tools/meson.ML;
|
file | diff | annotate |