Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
add lemmas singleton and insert_iff
2006-12-14, by huffman
generalized type of hyperpow; removed hcpow
2006-12-14, by huffman
redefine hSuc as *f* Suc, and move to HyperNat.thy
2006-12-14, by huffman
proper use of IntInf instead of InfInf;
2006-12-14, by wenzelm
defs/notes: more robust transitivity reasoning;
2006-12-14, by wenzelm
added trans_terms/props;
2006-12-14, by wenzelm
locale: print context for begin;
2006-12-14, by wenzelm
remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq
2006-12-14, by huffman
remove uses of star_n and FreeUltrafilterNat
2006-12-13, by huffman
remove use of FreeUltrafilterNat
2006-12-13, by huffman
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
2006-12-13, by huffman
fixed type
2006-12-13, by haftmann
added stub for OCaml serializer
2006-12-13, by haftmann
cleanup
2006-12-13, by haftmann
whitespace correction
2006-12-13, by haftmann
clarifed comment
2006-12-13, by haftmann
dropped FIXME comment
2006-12-13, by haftmann
clarified character setup
2006-12-13, by haftmann
remove references to star_n
2006-12-13, by huffman
SComplex abbreviates Standard
2006-12-13, by huffman
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
2006-12-13, by wenzelm
removed legacy ML bindings;
2006-12-13, by wenzelm
updated;
2006-12-13, by wenzelm
tuned signature;
2006-12-13, by wenzelm
internal_abbrev: observe print mode;
2006-12-13, by wenzelm
target_abbrev: internal mode for abbrevs;
2006-12-13, by wenzelm
edge: actually apply operation!
2006-12-13, by wenzelm
tuned;
2006-12-13, by wenzelm
authentic syntax for number_of
2006-12-13, by haftmann
introduced mk/dest_numeral/number for mk/dest_binum etc.
2006-12-13, by haftmann
fixed syntax for bounded quantification
2006-12-13, by haftmann
dropped superfluous header
2006-12-13, by haftmann
clarified error message
2006-12-13, by krauss
nat type now has a size functin => no longer needed as special case
2006-12-13, by krauss
simplified
2006-12-13, by krauss
local_abbrev: proper fix/declare of local entities;
2006-12-13, by wenzelm
Deleted the unused type argument of UVar
2006-12-13, by paulson
tuned comments;
2006-12-13, by wenzelm
added IsarAdvanced/Functions
2006-12-13, by krauss
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
2006-12-13, by huffman
remove uses of scaleR infix syntax; add lemma Reals_number_of
2006-12-13, by huffman
tuned;
2006-12-12, by wenzelm
add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
2006-12-12, by wenzelm
updated;
2006-12-12, by wenzelm
simplified unlocalize_mixfix;
2006-12-12, by wenzelm
removed is_class -- handled internally;
2006-12-12, by wenzelm
notation: Term.equiv_types;
2006-12-12, by wenzelm
abbrev: tuned signature;
2006-12-12, by wenzelm
tuned expand_term;
2006-12-12, by wenzelm
classified show/thus as prf_asm_goal, which is usually hilited in PG;
2006-12-12, by wenzelm
tuned expand_binds;
2006-12-12, by wenzelm
tuned error messages;
2006-12-12, by wenzelm
added equiv_types;
2006-12-12, by wenzelm
add_abbrev: tuned signature;
2006-12-12, by wenzelm
added expand_term_frees;
2006-12-12, by wenzelm
abbreviate: tuned signature;
2006-12-12, by wenzelm
LocalTheory.abbrev;
2006-12-12, by wenzelm
removed redundant constants and lemmas
2006-12-12, by huffman
additions to HOL-Complex
2006-12-12, by huffman
Removal of the "keep_types" flag: we always keep types!
2006-12-12, by paulson
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip