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 JavaScriptenabled browsers.
HOL_USEDIR_OPTIONS: no special M setting (now works with multithreaded);
20070827, by wenzelm
Added infinite_descent
20070827, by nipkow
updated keywords
20070827, by haftmann
added code_props
20070827, by haftmann
introduces params_of_sort
20070827, by haftmann
added simple definition scheme
20070827, by haftmann
added explicit equation for equality of nested environments
20070827, by haftmann
circumvented infix problem
20070827, by haftmann
tuned linear arith (once again) with ring_distribs
20070826, by nipkow
made SML/NJ happy
20070826, by haftmann
described 'rotated' attribute
20070826, by kleing
made SML/NJ happy
20070825, by haftmann
revised blacklisting for ATP linkup
20070824, by paulson
new derived rule: incr_type_indexes
20070824, by paulson
Returning both a "oneline" proof and a structured proof
20070824, by paulson
Reconstruction bug fix
20070824, by paulson
overloaded definitions accompanied by explicit constants
20070824, by haftmann
moved class dense_linear_order to Orderings.thy
20070824, by haftmann
updated
20070824, by haftmann
made sets executable
20070824, by haftmann
remove unused lemmas
20070824, by huffman
bin_sc_nth proof
20070824, by huffman
remove lemma bin_rec_PM
20070823, by huffman
avoid use of bin_rec_PM
20070823, by huffman
new instance proofs
20070823, by huffman
remove unused lemmas
20070823, by huffman
import BinInduct;
20070823, by huffman
declare bin_rest_BIT_bin_last [simp]
20070823, by huffman
Word/BinInduct.thy
20070823, by huffman
theory of integers as an inductive datatype
20070823, by huffman
move bin_nth stuff to its own subsection
20070823, by huffman
removed Word/Size.thy;
20070822, by huffman
typed print translation for CARD('a);
20070822, by huffman
rename type pls to num0
20070822, by huffman
move constant definitions to their respective subsections
20070822, by huffman
tuned;
20070822, by chaieb
More selective generalization : a*b is generalized whenever none of a and b is a number
20070822, by chaieb
imports Presburger; no need for Main
20070822, by chaieb
move bool list operations from WordBitwise to WordBoolList
20070822, by huffman
Word/WordBoolList.thy
20070822, by huffman
move if_simps from BinBoolList to Num_Lemmas
20070822, by huffman
Axioms for class no longer use objectuniversal quantifiers
20070822, by chaieb
move bool list stuff from WordDefinition and WordArith to new WordBoolList theory
20070822, by huffman
move bool list stuff from BinOperations to BinBoolList;
20070822, by huffman
Added mod cancellation simproc
20070821, by nipkow
remove redundant lemmas
20070821, by huffman
declare conj_absorb [simp]
20070821, by huffman
replace iszero_number_of_Pls with iszero_0 in rel_simps
20070821, by huffman
add lemma of_int_power
20070821, by huffman
Isarstyle proof for lfp_ordinal_induct
20070821, by huffman
ProofContext.restore_mode;
20070821, by wenzelm
added inner syntax mode, includes former type_mode and is_stmt;
20070821, by wenzelm
Modified message for sendback
20070821, by paulson
"sendback" to PG for oneline proof reconstructions
20070821, by paulson
Deleted the partiallytyped translation and the combinator code.
20070821, by paulson
move BIT datatype stuff from Num_Lemmas to BinGeneral
20070821, by huffman
simplify termination proof
20070821, by huffman
simplify proof of word_of_int
20070821, by huffman
improved evaluation interface
20070821, by haftmann
moved ordered_ab_semigroup_add to OrderedGroup.thy
20070821, by haftmann
less
more

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