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.
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
updated
20070821, by haftmann
move udvd, div and mod stuff from WordDefinition to WordArith
20070821, by huffman
move orderrelated stuff from WordDefinition to WordArith
20070821, by huffman
add lemma one_less_power
20070821, by huffman
move scast/ucast stuff to its own subsection
20070821, by huffman
move shiftingrelated constant definitions from WordDefinition to WordShift
20070821, by huffman
use HOLex later;
20070821, by wenzelm
standard_parse_term: added pp/check argument, include disambig here (from sign.ML);
20070820, by wenzelm
inner syntax: added parse_term/prop;
20070820, by wenzelm
read_def_terms: moved disambig to syntax.ML;
20070820, by wenzelm
tuned CRITICAL sections;
20070820, by wenzelm
remove redundant lemma int_number_of
20070820, by huffman
AC rules for bitwise logical operators no longer declared simp
20070820, by huffman
move bit simps from BinOperations to BitSyntax
20070820, by huffman
minimize imports
20070820, by huffman
reorganize into subsections
20070820, by huffman
prepare_dummies: NAMED_CRITICAL;
20070820, by wenzelm
with_modes []: noncritical;
20070820, by wenzelm
tuned signature;
20070820, by wenzelm
File.read/write/append: noncritical (basic IO operations already threadsafe);
20070820, by wenzelm
TextIO.inputLine: noncritical (assume exclusive ownership);
20070820, by wenzelm
tuned merge operations via pointer_eq;
20070820, by wenzelm
less
more

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