isabelle: Graph

merged
2010-11-15, by wenzelm
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
re-generalized type of prod_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
formal dependency on b2i files
2010-11-15, by boehmes
merged
2010-11-14, by boehmes
check the return code of the SMT solver and raise an exception if the prover failed
2010-11-12, by boehmes
updated README;
2010-11-14, by wenzelm
tuned;
2010-11-14, by wenzelm
cover 'write' as primitive proof command;
2010-11-14, by wenzelm
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
2010-11-14, by wenzelm
somewhat adhoc replacement for 'thus' and 'hence';
2010-11-13, by wenzelm
always print state of proof commands (notably "qed" etc.);
2010-11-13, by wenzelm
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
2010-11-13, by wenzelm
tuned message;
2010-11-13, by wenzelm
proper escape in regex;
2010-11-13, by wenzelm
report malformed symbols;
2010-11-13, by wenzelm
qualified Symbol_Pos.symbol;
2010-11-13, by wenzelm
total Symbol.source;
2010-11-13, by wenzelm
eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-11-13, by wenzelm
treat Unicode "replacement character" (i.e. decoding error) is malformed;
2010-11-13, by wenzelm
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
2010-11-13, by wenzelm
tuned;
2010-11-13, by wenzelm
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-13, by wenzelm
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
2010-11-13, by wenzelm
updated README;
2010-11-13, by wenzelm
defensive defaults for more robust experience for new users;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
preliminary support for newer versions of Z3
2010-11-12, by boehmes
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-12, by boehmes
let the theory formally depend on the Boogie output
2010-11-12, by boehmes
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
tuned;
2010-11-10, by wenzelm
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
2010-11-09, by wenzelm
updated version;
2010-11-09, by wenzelm
private counter, to keep externalized ids a bit smaller;
2010-11-09, by wenzelm
added general Synchronized.counter convenience;
2010-11-09, by wenzelm
explicitly identify forked/joined tasks;
2010-11-09, by wenzelm
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
2010-11-09, by wenzelm
merged
2010-11-09, by wenzelm
removed type-inference-like behaviour from relation_tac completely; tuned
2010-11-08, by krauss
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
2010-11-08, by wenzelm
explicitly check uniqueness of symbol recoding;
2010-11-08, by wenzelm
more hints on building and running Isabelle/jEdit from command line;
2010-11-08, by wenzelm
merged
2010-11-08, by wenzelm
merge
2010-11-08, by blanchet
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
2010-11-08, by blanchet
merged
2010-11-08, by huffman
merged
2010-11-06, by huffman
(infixl "<<" 55) -> (infix "<<" 50)
2010-11-05, by huffman
simplify some proofs
2010-11-03, by huffman
remove unnecessary stuff from Discrete.thy
2010-11-03, by huffman
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-11-03, by huffman
add lemma eq_imp_below
2010-11-03, by huffman
discontinue a bunch of legacy theorem names
2010-11-03, by huffman
move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-11-03, by huffman
simplify some proofs
2010-11-03, by huffman
compile -- 7550b2cba1cb broke the build
2010-11-08, by blanchet
merge
2010-11-08, by blanchet
recognize Vampire error
2010-11-08, by blanchet
return the process return code along with the process outputs
2010-11-08, by boehmes
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08, by boehmes