Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+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.
Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05, by wenzelm
close_schematic_term: uniform order of types/terms;
2009-03-05, by wenzelm
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05, by wenzelm
TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
2009-03-05, by wenzelm
fixed proofs -- follow-up to ecd6f0ca62ea;
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name");
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name;
2009-03-05, by wenzelm
eliminated obsolete ProofContext.full_bname;
2009-03-05, by wenzelm
Binding.prefix_of;
2009-03-05, by wenzelm
adapted Binding.dest;
2009-03-05, by wenzelm
added prefix_of;
2009-03-05, by wenzelm
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-05, by blanchet
merged
2009-03-05, by wenzelm
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04, by huffman
regenerated document;
2009-03-05, by wenzelm
merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
2009-03-05, by wenzelm
dummy changes to produce a new changeset of these files;
2009-03-05, by wenzelm
updated generated file -- changed since @{ML} now ignores source flag;
2009-03-05, by wenzelm
fixed document;
2009-03-05, by wenzelm
removed old/broken CVS Ids;
2009-03-04, by wenzelm
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
2009-03-04, by wenzelm
merged
2009-03-04, by chaieb
Moved general theorems about sums and products to FiniteSet.thy
2009-03-04, by chaieb
fixed proofs; added rules as default simp-rules
2009-03-04, by chaieb
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
2009-03-04, by chaieb
Added Libray dependency on Topology_Euclidean_Space
2009-03-04, by chaieb
Added general theorems for fold_image, setsum and set_prod
2009-03-04, by chaieb
fixed proofs
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-02-25, by chaieb
merged
2009-02-25, by chaieb
Second try at adding "nitpick_const_def" attribute.
2009-03-04, by blanchet
Fix parentheses.
2009-03-04, by blanchet
merged
2009-03-04, by blanchet
Added "nitpick_const_simp" attribute to Nominal primrec.
2009-03-04, by blanchet
NEWS: renamed o2s to Option.set;
2009-03-04, by wenzelm
less arbitrary occurrences of undefined
2009-03-04, by haftmann
datatype antiquotation does not assume LaTeX as output any longer
2009-03-04, by haftmann
merged
2009-03-04, by nipkow
Option.thy
2009-03-04, by nipkow
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
2009-03-04, by haftmann
merged
2009-03-04, by haftmann
explicit error message for `improper` instances lacking explicit instance parameter constants
2009-03-04, by haftmann
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Made Refute.norm_rhs public, so I can use it in Nitpick.
2009-03-04, by blanchet
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
2009-03-01, by blanchet
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
2009-02-24, by blanchet
merged
2009-03-04, by nipkow
Made Option a separate theory and renamed option_map to Option.map
2009-03-04, by nipkow
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-04, by wenzelm
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
2009-03-03, by wenzelm
tuned str_of, now subject to verbose flag;
2009-03-03, by wenzelm
added @{binding} ML antiquotations;
2009-03-03, by wenzelm
added print_properties, print_position (again);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
merged
2009-03-03, by haftmann
tuned manuals
2009-03-03, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip