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.
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
Overloading of "^" requires a type constraint
19970530, by paulson
Overloading of "^" requires new type class "power", with types "nat" and
19970530, by paulson
New theory Divides
19970530, by paulson
Many new theorems about cardinality
19970530, by paulson
Now Divides must be the parent
19970530, by paulson
Moving div and mod from Arith to Divides
19970530, by paulson
flushOut ensures that no recent error message are lost (not certain this is
19970530, by paulson
polyml3.1 default again (for local work);
19970527, by wenzelm
fixed P (checkout only);
19970527, by wenzelm
NJ 1.09.2x as factory default!
Isabelle948
19970527, by wenzelm
Last changes for new release 948
19970527, by mueller
added 1.09.28 note;
19970527, by wenzelm
New theorems suggested by Florian Kammueller
19970527, by paulson
Restoration of the two "bypassed" theorems Union_quotient and quotient_disj
19970527, by paulson
Removal of card_insert_disjoint, which is now a default rewrite rule
19970527, by paulson
New theorem disjoint_eq_subset_Compl
19970527, by paulson
New theorem le_Suc_eq
19970527, by paulson
Removal of mask.sig and mask.sml
19970527, by paulson
Removal of module Mask and datatype binding with its constructor >
19970527, by paulson
New theorems suggested by Florian Kammueller
19970527, by paulson
remoded ccc1
19970526, by slotosch
removed ccc1
19970526, by slotosch
tuned comment;
19970526, by wenzelm
Two useful facts about Powersets suggested by Florian Kammueller
19970526, by paulson
Added a missing "result();" after problem 43.
19970526, by paulson
Tidying using the new exhaust_tac
19970526, by paulson
Now recdef checks the name of the function being defined.
19970526, by paulson
Deleted option_case_tac because exhaust_tac performs a similar function.
19970526, by paulson
Renamed lessD to Suc_leI
19970526, by paulson
New operator "lists" for formalizing sets of lists
19970526, by paulson
New theorem subset_inj_onto
19970526, by paulson
Two results suggested by Florian Kammueller
19970526, by paulson
Tidying and a couple of useful lemmas
19970526, by paulson
Added recdef
19970526, by paulson
Primrec: New example ported from ZF
19970526, by paulson
Renamed lessD to Suc_leI
19970526, by paulson
New example ported from ZF
19970526, by paulson
Simplified proofs using expand_option_case
19970526, by paulson
Now checks the name of the function being defined;
19970526, by paulson
More deHOLification
19970526, by paulson
Now checks the name of the function being defined
19970526, by paulson
Deleted unused functions
19970526, by paulson
Now a Perl script. No longer requires commands to be at the beginnings of
19970526, by paulson
Slight simplifications
19970526, by paulson
Eliminated ccc1. Moved ID,oo into Cfun.
19970525, by slotosch
Moved the classes flat chfin from Fix to Pcpo.
19970525, by slotosch
*** empty log message ***
19970525, by slotosch
Eliminated the prediates flat,chfin
19970525, by slotosch
less
more

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