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.
use consts for infix syntax
20051106, by huffman
add proof of Bekic's theorem: fix_cprod
20051106, by huffman
simplify definitions
20051105, by huffman
put iterate and fix in separate sections; added Letrec
20051105, by huffman
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
20051105, by huffman
add line breaks to Rep_CFun syntax
20051105, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy; moved admwrelated stuff to its own section
20051104, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy
20051104, by huffman
cleaned up
20051104, by huffman
add print translation: Abs_CFun f => LAM x. f x
20051104, 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.
20051103, by mengj
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutuallyrecursive types; initial support for indirect recursion
20051103, by huffman
reimplement copy_def to use data constructor constants
20051103, by huffman
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
20051103, by huffman
generate lambda pattern syntax for new data constructors
20051103, by huffman
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
20051103, by huffman
add constant one_when; LAM pattern for ONE
20051103, by huffman
add translation for wildcard pattern
20051103, by huffman
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
20051103, by huffman
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
20051103, by huffman
cleaned up; ch2ch_Rep_CFun is a simp rule
20051103, by huffman
changed iterate to a continuous type
20051103, by huffman
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
20051103, by huffman
removed ex/loeckx.ML
20051103, by huffman
removed proof about Ifix, which no longer exists
20051103, by huffman
cleaned up; chain_const and thelub_const are simp rules
20051103, by huffman
cleaned up; removed adm_tricks in favor of compactness theorems
20051103, by huffman
fix spelling
20051102, by huffman
Moved atom stuff to new file nominal_atoms.ML
20051102, by berghofe
 completed the list of thms for supp_atm
20051102, by urbanc
Added code for proving that new datatype has finite support.
20051102, by berghofe
removed unused modify_typargs, map_typargs, fold_typargs;
20051102, by wenzelm
added Isar.state/exn;
20051102, by wenzelm
Isar.loop;
20051102, by wenzelm
moved consts declarations to consts.ML;
20051102, by wenzelm
Consts.dest;
20051102, by wenzelm
Polymorphic constants.
20051102, by wenzelm
added consts.ML;
20051102, by wenzelm
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
20051102, by wenzelm
dist_eqI: the_context();
20051102, by wenzelm
Sign.const_monomorphic;
20051102, by wenzelm
Logic.nth_prem;
20051102, by wenzelm
added the collection of lemmas "supp_at"
20051102, by urbanc
some minor tweaks in some proofs (nothing extraordinary)
20051101, by urbanc
tunings of some comments (nothing serious)
20051101, by urbanc
nth_*, fold_index refined
20051031, by haftmann
fold_index replacing foldln
20051031, by haftmann
A few new lemmas
20051031, by nipkow
tuned my last commit
20051030, by urbanc
simplified the abs_supp_approx proof and tuned some comments in
20051030, by urbanc
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
20051029, by urbanc
1) have adjusted the swapping of the result type
20051029, by urbanc
tuned;
20051028, by wenzelm
lthms_containing: not o valid_thms;
20051028, by wenzelm
added fact_tac, some_fact_tac;
20051028, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
20051028, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
20051028, by wenzelm
added fact method;
20051028, by wenzelm
tuned ProofContext.export interfaces;
20051028, by wenzelm
syntax for literal facts;
20051028, by wenzelm
less
more

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