Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-50
-24
+24
+50
+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 JavaScript-enabled browsers.
Added strong induction theorem (currently only axiomatized!).
2005-11-07, by berghofe
Initial commit.
2005-11-07, by urbanc
Initial commit of the theory "Weakening".
2005-11-07, by urbanc
added thms perm, distinct and fresh to the simplifier.
2005-11-07, by urbanc
added proper fillin_mixfix
2005-11-07, by haftmann
added fillin_mixfix, replace_quote
2005-11-07, by haftmann
New function store_thmss_atts.
2005-11-07, by berghofe
used the function Library.product for the cprod from Stefan
2005-11-07, by urbanc
fixed bug with nominal induct
2005-11-07, by urbanc
added fillin_mixfix' needed by serializer
2005-11-07, by haftmann
add case syntax stuff
2005-11-06, by huffman
use consts for infix syntax
2005-11-06, by huffman
add proof of Bekic's theorem: fix_cprod
2005-11-06, by huffman
simplify definitions
2005-11-05, by huffman
put iterate and fix in separate sections; added Letrec
2005-11-05, by huffman
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-05, by huffman
add line breaks to Rep_CFun syntax
2005-11-05, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
2005-11-04, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy
2005-11-04, by huffman
cleaned up
2005-11-04, by huffman
add print translation: Abs_CFun f => LAM x. f x
2005-11-04, by huffman
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
2005-11-03, by mengj
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
2005-11-03, by huffman
reimplement copy_def to use data constructor constants
2005-11-03, by huffman
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-50
-24
+24
+50
+100
+300
+1000
+3000
+10000
+30000
tip