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 JavaScript-enabled browsers.
avoid prove_plain, export_plain, simplified after_qed;
2005-11-08, by wenzelm
removed export_plain;
2005-11-08, by wenzelm
renamed assert_prop to ensure_prop;
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
export compose_hhf;
2005-11-08, by wenzelm
removed impose_hyps, satisfy_hyps;
2005-11-08, by wenzelm
const args: do not store variable names (unused);
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
(fix for accidental commit)
2005-11-08, by haftmann
(codegen)
2005-11-08, by haftmann
generate pattern combinators for new datatypes
2005-11-08, by huffman
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
2005-11-07, by huffman
add case syntax for type one
2005-11-07, by huffman
remove syntax for as-patterns
2005-11-07, by huffman
avoid 'as' as identifier;
2005-11-07, by wenzelm
avoid 'as' as identifier;
2005-11-07, by wenzelm
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
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
2005-11-03, by huffman
generate lambda pattern syntax for new data constructors
2005-11-03, by huffman
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
2005-11-03, by huffman
add constant one_when; LAM pattern for ONE
2005-11-03, by huffman
add translation for wildcard pattern
2005-11-03, by huffman
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-11-03, by huffman
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
2005-11-03, by huffman
cleaned up; ch2ch_Rep_CFun is a simp rule
2005-11-03, by huffman
changed iterate to a continuous type
2005-11-03, by huffman
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
2005-11-03, by huffman
removed ex/loeckx.ML
2005-11-03, by huffman
removed proof about Ifix, which no longer exists
2005-11-03, by huffman
cleaned up; chain_const and thelub_const are simp rules
2005-11-03, by huffman
cleaned up; removed adm_tricks in favor of compactness theorems
2005-11-03, by huffman
fix spelling
2005-11-02, by huffman
Moved atom stuff to new file nominal_atoms.ML
2005-11-02, by berghofe
- completed the list of thms for supp_atm
2005-11-02, by urbanc
Added code for proving that new datatype has finite support.
2005-11-02, by berghofe
removed unused modify_typargs, map_typargs, fold_typargs;
2005-11-02, by wenzelm
added Isar.state/exn;
2005-11-02, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip