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.
nnf_simpset built statically
20061004, by webertj
rewrite proofs of powser_insidea and termdiffs_aux
20061003, by huffman
generalize summability lemmas using class banach
20061002, by huffman
clarified setup name
20061002, by haftmann
various code refinements
20061002, by haftmann
fixed some Haskell issues
20061002, by haftmann
changed preprocessing framework
20061002, by haftmann
clarified some things
20061002, by haftmann
cleaned and extended
20061002, by haftmann
added gen_primrec
20061002, by haftmann
added code for insert
20061002, by haftmann
improvements for code_gen
20061002, by haftmann
cleaned mess
20061002, by haftmann
added example for code_gen
20061002, by haftmann
dropped obsolete Theory.sign_of
20061002, by haftmann
tuned
20061002, by haftmann
added code generator names for nat_rec and nat_case
20061002, by haftmann
improved serialization for arbitrary
20061002, by haftmann
normal_form now a diagnostic command
20061002, by haftmann
restructured contents
20061002, by haftmann
add axclass banach for complete normed vector spaces
20061002, by huffman
remove unused Cauchy_Bseq lemmas
20061002, by huffman
add lemmas norm_not_less_zero, norm_le_zero_iff
20061002, by huffman
added is_Trueprop
20061002, by paulson
tidying and simplifying
20061002, by paulson
Changing the default for theory_const
20061002, by paulson
extensions for Susanto
20061002, by paulson
restored the "length of name > 2" check for package definitions
20061002, by paulson
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
20061002, by paulson
exists_name: include this theory name;
20061001, by wenzelm
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
20061001, by wenzelm
merged with theory Datatype_Universe;
20061001, by wenzelm
obsolete;
20061001, by wenzelm
renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
20061001, by wenzelm
removed share_data;
20061001, by wenzelm
cterm_match: avoid recalculation of maxidx;
20061001, by wenzelm
reverted to revision 1.28;
20061001, by wenzelm
proper use of svc_oracle.ML;
20061001, by wenzelm
reactivated theory PER;
20061001, by wenzelm
tuned proofs;
20061001, by wenzelm
moved theory Infinite_Set to Library;
20061001, by wenzelm
moved theory Infinite_Set to Library;
20061001, by wenzelm
moved Infinite_Set.thy to Library;
20061001, by wenzelm
tuned;
20061001, by wenzelm
Removed the helper files (combinator rewrite rules, function extensionality and fequal rules).
20061001, by mengj
generalize more DERIV proofs
20061001, by huffman
statement: Variable.fix_frees;
20060930, by wenzelm
added undo_end;
20060930, by wenzelm
tuned proofs;
20060930, by wenzelm
proper import of Main HOL;
20060930, by wenzelm
tuned specifications and proofs;
20060930, by wenzelm
hides popular names (from Datatype.thy);
20060930, by wenzelm
removed obsolete sum_case_Inl/Inr;
20060930, by wenzelm
renamed Variable.invent_fixes to Variable.variant_fixes;
20060930, by wenzelm
generalize proofs of DERIV_isCont and DERIV_mult
20060930, by huffman
generalized some DERIV proofs
20060930, by huffman
add scaleR lemmas
20060930, by huffman
generalize type of DERIV
20060930, by huffman
add type annotations for DERIV
20060930, by huffman
Combinator axioms are now from Isabelle theorems, no need to use helper files.
20060930, by mengj
less
more

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