Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
2010-03-08
huffman
construct fully typed goal in proof of induction rule
changeset
|
files
2010-03-08
huffman
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
changeset
|
files
2010-03-08
huffman
remove redundant function arguments
changeset
|
files
2010-03-08
huffman
include take_info within take_induct_info type
changeset
|
files
2010-03-08
huffman
pass take_info as an argument to comp_theorems
changeset
|
files
2010-03-08
huffman
pass take_induct_info as an argument to comp_theorems
changeset
|
files
2010-03-08
huffman
add type take_induct_info
changeset
|
files
2010-03-08
huffman
generate take_induct lemmas
changeset
|
files
2010-03-08
huffman
move proofs of reach and take lemmas to domain_take_proofs.ML
changeset
|
files
2010-03-08
huffman
move lemmas from Domain.thy to Domain_Aux.thy
changeset
|
files
2010-03-08
huffman
move take-proofs stuff into new theory Domain_Aux.thy
changeset
|
files
2010-03-08
huffman
add type take_info
changeset
|
files
2010-03-08
huffman
add function add_qualified_def
changeset
|
files
2010-03-08
haftmann
merged
changeset
|
files
2010-03-08
haftmann
proper ML interface; further polishing
changeset
|
files
2010-03-08
haftmann
code simplification and tuning
changeset
|
files
2010-03-08
berghofe
Added inducts field to inductive_result.
changeset
|
files
2010-03-08
haftmann
transfer: avoid camel case, more standard coding conventions, misc tuning
changeset
|
files
2010-03-08
haftmann
transfer: avoid camel case
changeset
|
files
2010-03-08
huffman
merged
changeset
|
files
2010-03-08
huffman
generate separate qualified theorem name for each type's reach and take_lemma
changeset
|
files
2010-03-08
huffman
add simp rule LAM_strict
changeset
|
files
2010-03-07
huffman
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
changeset
|
files
2010-03-07
haftmann
merged
changeset
|
files
2010-03-07
haftmann
dropped dead code; adhere more closely to standard coding conventions
changeset
|
files
2010-03-07
huffman
merged
changeset
|
files
2010-03-07
huffman
arith tactic uses 'priority' instead of 'warning' to print messages
changeset
|
files
2010-03-07
huffman
add simp rules about Ints, Nats
changeset
|
files
Loading...
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip