isabelle: Graph

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

look for certificates relative to the theory
2010-11-12, by boehmes
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
2010-11-12, by boehmes
merged
2010-11-12, by huffman
update Theory.requires with new theory name
2010-11-12, by huffman
tuned signatures;
2010-11-12, by wenzelm
never open Unsynchronized;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
section headings
2010-11-10, by huffman
reorder chapters for generated document
2010-11-10, by huffman
merge Representable.thy into Domain.thy
2010-11-10, by huffman
move stuff from Domain.thy to Domain_Aux.thy
2010-11-10, by huffman
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-11-10, by huffman
allow unpointed lazy arguments for definitional domain package
2010-11-10, by huffman
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
2010-11-10, by huffman
merged
2010-11-10, by huffman
removed unused lemma chain_mono2
2010-11-10, by huffman
rename class 'bifinite' to 'domain'
2010-11-10, by huffman
instance sum :: (predomain, predomain) predomain
2010-11-10, by huffman
configure sum type for fixrec
2010-11-10, by huffman
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
2010-11-10, by huffman
instance prod :: (predomain, predomain) predomain
2010-11-10, by huffman
adapt isodefl proof script to unpointed types
2010-11-09, by huffman
add 'predomain' class: unpointed version of bifinite
2010-11-09, by huffman
add bifiniteness check for domain_isomorphism command
2010-11-09, by huffman
implement map_of_typ using Pattern.rewrite_term
2010-11-09, by huffman
avoid using stale theory
2010-11-09, by huffman
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
2010-11-08, by huffman
add function the_sort
2010-11-08, by huffman
refactor tmp_thy code
2010-11-08, by huffman
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
2010-11-08, by huffman
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
2010-11-12, by wenzelm
Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
2010-11-12, by wenzelm
more precise treatment of deleted nodes;
2010-11-11, by wenzelm
tuned error message;
2010-11-11, by wenzelm
unified type Document.Edit;
2010-11-11, by wenzelm
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
2010-11-11, by wenzelm
tuned;
2010-11-11, by wenzelm
reduced danger of line breaks within minipage;
2010-11-11, by wenzelm
Sidekick block asset: show first line only;
2010-11-10, by wenzelm
added buffer_text convenience, with explicit locking;
2010-11-10, by wenzelm
use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
2010-11-10, by wenzelm
merged
2010-11-10, by wenzelm
make SML/NJ happy
2010-11-10, by blanchet
merged
2010-11-09, by haftmann
slightly changed fun_map_def
2010-11-09, by haftmann
fun_rel_def is no simp rule by default
2010-11-09, by haftmann
more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
2010-11-09, by haftmann
more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
type annotations in specifications; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
fun_rel_def is no simp rule by default
2010-11-09, by haftmann
merged
2010-11-09, by paulson
tidied using metis
2010-11-09, by paulson
manage folding via sidekick by default;
2010-11-10, by wenzelm
eliminated obsolete heading category -- superseded by heading_level;
2010-11-10, by wenzelm
treat main theory commands like headings, and nest anything else inside;
2010-11-10, by wenzelm
proper treatment of equal heading level;
2010-11-10, by wenzelm
added missing Keyword.THY_SCHEMATIC_GOAL;
2010-11-10, by wenzelm
default Sidekick parser based on section headings;
2010-11-10, by wenzelm
some support for nested source structure, based on section headings;
2010-11-10, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle