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.
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
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
20070416, by urbanc
added a more usuable lemma for dealing with fresh_fun
20070416, by urbanc
generalized type of lemma geometric_sum
20070416, by huffman
replaced read_term_legacy by read_prop_legacy;
20070415, by wenzelm
removed obsolete redeclare_skolems;
20070415, by wenzelm
read prop as prop, not term;
20070415, by wenzelm
removed obsolete TypeInfer.logicT  use dummyT;
20070415, by wenzelm
avoid internal names;
20070415, by wenzelm
tuned;
20070415, by wenzelm
legacy_infer_term/prop  including intern_term;
20070415, by wenzelm
Thm.plain_prop_of;
20070415, by wenzelm
added decode_types (from type_infer.ML);
20070415, by wenzelm
added read_term;
20070415, by wenzelm
added mixfixT (from type_infer.ML);
20070415, by wenzelm
proper interface infer_types(_pat);
20070415, by wenzelm
Thm.fold_terms;
20070415, by wenzelm
removed unused Output.panic hook  internal to PG wrapper;
20070415, by wenzelm
moved get_sort to sign.ML;
20070415, by wenzelm
removed obsolete inferT_axm;
20070415, by wenzelm
removed obsolete infer_types(_simult);
20070415, by wenzelm
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
20070415, by wenzelm
load type_infer.ML early;
20070415, by wenzelm
adapted decode_type;
20070415, by wenzelm
proper ProofContext.infer_types;
20070415, by wenzelm
Thm.fold_terms;
20070415, by wenzelm
less
more

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