Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
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.
WWW_Find component: find_theorems via web browser
20091120, by kleing
merged
20091120, by wenzelm
merged
20091120, by nipkow
Rene tuned proof
20091120, by nipkow
example theory for new domain package
20091120, by huffman
thy_decl outer syntax for repdef
20091119, by huffman
merged
20091119, by huffman
nicer warning message for indirectrecursive domain definitions
20091119, by huffman
store map_ID thms in theory data; automate proofs of reach lemmas
20091119, by huffman
add map_ID lemmas
20091119, by huffman
domain_isomorphism package defines combined copy function
20091119, by huffman
merged
20091120, by nipkow
added Rene Thiemann's normalize function
20091120, by nipkow
added lemma
20091120, by nipkow
merged
20091119, by huffman
domain_isomorphism package defines copy functions
20091119, by huffman
copy_of_dtyp uses map table from theory data
20091119, by huffman
Domain.thy imports Representable.thy
20091119, by huffman
fix definitions of copy combinators
20091119, by huffman
clean up indentation; add 'definitional' option flag
20091119, by huffman
rename generated abs_iso, rep_iso lemmas
20091119, by huffman
clean up indentation
20091119, by huffman
add dependency on domain_isomorphism.ML
20091119, by huffman
set up domain_isomorphism package in Representable.thy
20091119, by huffman
automate proofs of map_ID theorems
20091119, by huffman
change Theory.requires
20091119, by huffman
use theory data for REP_simps and isodefl_rules
20091119, by huffman
replace defl_tab and map_tab with theory data
20091119, by huffman
separate conjuncts of isodefl theorem
20091119, by huffman
automate isodefl proof
20091119, by huffman
change example to use recursion with continuous function space
20091119, by huffman
add lemma isodefl_cprod
20091119, by huffman
automate definition of map functions; remove unused code
20091119, by huffman
change naming convention for deflation combinators
20091119, by huffman
add new makefile dependencies
20091119, by huffman
prove isomorphism and isodefl rules
20091119, by huffman
avoid using csplit; define copy functions exactly like the current domain package
20091119, by huffman
merged
20091119, by huffman
remove one_typ and tr_typ; add abs/rep lemmas
20091118, by huffman
automate definition of rep/abs functions
20091118, by huffman
get rid of numbers on thy variables
20091118, by huffman
automate proofs of REP equations
20091118, by huffman
cleaned up; factored out fixedpoint definition code
20091118, by huffman
automate solution of domain equations
20091118, by huffman
removed fixme  quickanddirty flag is appropriate
20091120, by Christian Urban
use of thmantiquotation
20091120, by Christian Urban
Added new counterexample generator SML_inductive for goals involving
20091119, by berghofe
Added infrastructure for embedding random data generators into code generated
20091119, by berghofe
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
20091119, by wenzelm
future_result: purge flexflex pairs, which should normally be trivial anyway  prevent Thm.future_result from complaining about tpairs;
20091119, by wenzelm
toplevel pretty printer for Synchronized.var;
20091119, by wenzelm
adapted Local_Theory.define  eliminated odd thm kind;
20091119, by wenzelm
Specification.definition: Thm.definitionK marks exactly the highlevel enduser result;
20091119, by wenzelm
Local_Theory.define: eliminated slightly odd kind argument  such lowlevel definitions should be hardly ever exposed to endusers anyway;
20091119, by wenzelm
merged
20091119, by wenzelm
merged
20091119, by paulson
Minor correction
20091119, by paulson
some attempts to improve termination of isatest;
20091119, by wenzelm
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
20091119, by hoelzl
Renamed vector_less_eq_def to the more usual name vector_le_def.
20091119, by hoelzl
less
more

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