Mercurial
Mercurial
>
repos
>
testboard
/ 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.
encode clauses as Isar premises, rather than as objectlogic &, for faster parsing
20060828, by webertj
abstraction of lambdaexpressions
20060825, by paulson
tidied
20060825, by paulson
better skolemization, using firstorder resolution rather than hoping for the right result
20060825, by paulson
using inc
20060825, by paulson
explicit type variables prevent empty sorts
20060825, by paulson
replaced skolem declarations by automatic skolemization of everything
20060825, by paulson
avoid duplicate tactics
20060825, by webertj
additional list of tactics that can be added to arith
20060824, by webertj
Added premises concerning finite support of recursion results to FCBs.
20060824, by berghofe
speed up proof of summable_Cauchy
20060823, by huffman
speed up some proofs
20060823, by huffman
generalize proof of SUP_rabs_subseq
20060823, by huffman
speed up some proofs
20060823, by huffman
SML/NJ int type fix
20060823, by haftmann
tracing
20060821, by haftmann
improved preprocessing
20060821, by haftmann
fixed bug in sortlookup
20060821, by haftmann
more concise preprocessing of numerals for code generation
20060821, by haftmann
more concise string serialization
20060821, by haftmann
added some codegen examples/applications
20060821, by haftmann
adapted using the characteristic equations
20060818, by urbanc
modified to use the characteristic equations
20060818, by urbanc
 Fixed bug that caused uniqueness proof for recursion
20060818, by berghofe
used the recursion combinator for the height and substitution function
20060817, by urbanc
added definition for size and substitution using the recursion
20060817, by urbanc
improved thmtab
20060817, by haftmann
fixed bug in sortcontext extraction
20060817, by haftmann
dropped definitions_of
20060817, by haftmann
added all_super_classes
20060817, by haftmann
renamed module to thyname
20060817, by haftmann
cleanup
20060817, by haftmann
added missing supp_nat lemma
20060816, by urbanc
added
20060814, by haftmann
module restructuring
20060814, by haftmann
code cleanup, instance_subsort now working
20060814, by haftmann
added code generator packages
20060814, by haftmann
adaptions to improvements
20060814, by haftmann
added add_hook_bootstrap
20060814, by haftmann
added new files
20060814, by haftmann
simplified code generator setup
20060814, by haftmann
added passage on class package
20060814, by haftmann
updated code generator keywords
20060814, by haftmann
Removed nontrivial definitions from calc_atm theorem list.
20060814, by berghofe
Finished implementation of uniqueness proof for recursion combinator.
20060814, by berghofe
*** empty log message ***
20060814, by chaieb
Reification now handels binders.
20060814, by chaieb
consistent prefixing for skolem functions
20060809, by paulson
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
20060809, by paulson
tuned: string_of_list, string_of_pair
20060809, by webertj
* ProofContext.prems_limit is now 1 by default;
20060809, by wenzelm
tuned proofs;
20060809, by wenzelm
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
20060809, by wenzelm
renamed map_theory to theory;
20060809, by wenzelm
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
20060809, by wenzelm
locale interpretation command: after_qed;
20060809, by wenzelm
int_option: signed_string_of_int;
20060809, by wenzelm
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
20060809, by wenzelm
skolem declarations for builtin theorems
20060808, by paulson
more explict variable names
20060808, by paulson
less
more

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