Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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 JavaScriptenabled browsers.
Useful new lemma
19970609, by paulson
eliminated nonASCII;
19970606, by wenzelm
Added
19970606, by nipkow
improved function 'nonreserved'
19970606, by oheimb
Removed a few redundant additions of simprules or classical rules
19970606, by paulson
The name bex_conj_distrib was WRONG
19970606, by paulson
Better miniscoping for bounded quantifiers
19970606, by paulson
Tidying and simplification of declarations
19970606, by paulson
Much polishing of proofs
19970606, by paulson
New miniscoping rules for ALL
19970606, by paulson
New facts about In0/1 by Burkhart Wolff
19970606, by paulson
New miniscoping rules ball_triv and bex_triv
19970606, by paulson
Mended the definition of ack(0,n)
19970606, by paulson
Two new examples; corrected a comment
19970606, by paulson
New example theory: Recdef
19970606, by paulson
added finite_converse
19970605, by nipkow
Moved image_is_empty from Finite.ML to equalities.ML
19970605, by nipkow
Modified a few defs and proofs because of the changes to theory Finite.thy.
19970605, by nipkow
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
19970605, by nipkow
New recdef examples
19970605, by paulson
Removal of freeze_vars and thaw_vars. New freeze_thaw
19970605, by paulson
freezeT now refers to Type.freeze_thaw
19970605, by paulson
Tidying of signature. More robust renaming in freeze_thaw.
19970605, by paulson
Removal of freeze_vars and thaw_vars (quite unused...)
19970605, by paulson
Removal of radixstring from string_of_int; addition of string_of_indexname
19970605, by paulson
There was never need for another copy of radixstring...
19970605, by paulson
Numerous simplifications and removal of HOLisms
19970605, by paulson
Now loads theory Recdef
19970605, by paulson
A slight simplification of optstring
19970605, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
19970605, by paulson
Deleted the obsolete "pred_list" relation
19970605, by paulson
Documented the new distinct_subgoals_tac
19970605, by paulson
A slight simplification of optstring
19970605, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
19970605, by paulson
Made the pseudotype of split_rule_var a separate argument
19970605, by paulson
eliminated nonASCII;
19970604, by wenzelm
eliminated freeze_vars;
19970604, by wenzelm
changed priority of > from [6,5]5 to [1,0]0
19970604, by mueller
is_blank: fixed space2;
19970603, by wenzelm
No longer refers to internal TFL structures
19970603, by paulson
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
19970603, by paulson
New theory "Power" of exponentiation (and binomial coefficients)
19970603, by paulson
New theorem about the cardinality of the powerset (uses exponentiation)
19970603, by paulson
Type inference makes a Const here, perhaps elsewhere?thry.sml
19970602, by paulson
poly_tvars allows recdefs to be made without type constraints
19970602, by paulson
Corrected banner: it is W0, not MiniML
19970602, by paulson
New statement and proof of free_tv_subst_var in order to cope with new
19970602, by paulson
Now Un_insert_left, Un_insert_right are default rewrite rules
19970602, by paulson
Corrected statement of filter_append; added filter_size
19970602, by paulson
Simplified proof
19970602, by paulson
New theorems le_add_diff_inverse, le_add_diff_inverse2
19970602, by paulson
trivial changes to incorporate CTL.thy and Example.ML in html file;
19970530, by mueller
Simplified the calling sequence of CONTEXT_REWRITE_RULE
19970530, by paulson
Moved "less_eq" to NatDef from Arith
19970530, by paulson
New results including the basis for unique factorization
19970530, by paulson
Now "primes" is a set
19970530, by paulson
Now Divides must be the parent
19970530, by paulson
New proofs about cardinality. Suggested by Florian Kammueller
19970530, by paulson
Addition of Finite as parent allows cardinality theorems
19970530, by paulson
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
19970530, by paulson
less
more

(0)
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip