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.
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
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
less
more

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