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.
oups : wrong commit
20070424, by narboux
adds op in front of an infix to fix SML compilation
20070424, by narboux
sane version of read_termTs (proper freeze);
20070423, by wenzelm
read_instantiations: proper typeinference with fixed variables, infer parameter types as well;
20070423, by wenzelm
added paramify_vars;
20070423, by wenzelm
def_simproc(_i): proper ProofContext.read/cert_terms;
20070423, by wenzelm
simplified ProofContext.read_termTs;
20070423, by wenzelm
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
20070423, by urbanc
initial commit
20070423, by haftmann
faster proof of wf_eq_minimal
20070421, by huffman
export get_sort (belongs to Syntax module);
20070421, by wenzelm
TypeExt.decode_term;
20070421, by wenzelm
added decode_term (belongs to Syntax module);
20070421, by wenzelm
tuned the setup of fresh_fun
20070421, by urbanc
defs are added to code data
20070420, by haftmann
repaired value restriction problem
20070420, by haftmann
reverted to classical syntax for K_record
20070420, by haftmann
tuned
20070420, by haftmann
Interpretation equations applied to attributes
20070420, by ballarin
Interpretation equations applied to attributes;
20070420, by ballarin
Modified eqvt_tac to avoid failure due to introduction rules
20070420, by berghofe
clarifed
20070420, by haftmann
modify fresh_fun_simp to ease debugging
20070420, by narboux
updated code generator
20070420, by haftmann
updated
20070420, by haftmann
adds extracted program to code theorem table
20070420, by haftmann
unfold attribute now also accepts HOL equations
20070420, by haftmann
added more stuff
20070420, by haftmann
add definitions explicitly to code generator table
20070420, by haftmann
cleared dead code
20070420, by haftmann
moved axclass module closer to core system
20070420, by haftmann
Isar definitions are now added explicitly to code theorem table
20070420, by haftmann
improved case unfolding
20070420, by haftmann
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
20070420, by haftmann
tuned syntax: K_record is now an authentic constant
20070420, by haftmann
tuned: now using function package
20070420, by haftmann
transfer_tac accepts also HOL equations as theorems
20070420, by haftmann
shifted min/max to class order
20070420, by haftmann
tuned
20070420, by haftmann
added class tutorial
20070420, by haftmann
code generator changes
20070420, by haftmann
generate page labels
20070420, by krauss
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
20070420, by krauss
declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)
20070420, by urbanc
trying to make singlestep proofs work better, especially if they contain
20070419, by paulson
nominal_inductive no longer proves equivariance.
20070419, by berghofe
add a tactic to generate fresh names
20070419, by narboux
simplified ProofContext.infer_types(_pats);
20070418, by wenzelm
Improved comments.
20070418, by dixon
proper header, added regression tests
20070418, by krauss
added temporary hack to avoid schematic goals in "termination".
20070418, by krauss
Fixes for proof reconstruction, especially involving abstractions and definitions
20070418, by paulson
export is_dummy_pattern;
20070417, by wenzelm
lemma isCont_inv_fun is same as isCont_inverse_function
20070417, by huffman
moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
20070417, by huffman
remove use of pos_boundedE
20070417, by huffman
lemma geometric_sum no longer needs class division_by_zero
20070417, by huffman
tuned proofs;
20070417, by wenzelm
canonical merge operations
20070416, by haftmann
added print_indexname;
20070416, by wenzelm
less
more

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