isabelle: Graph

do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
2010-10-27, by blanchet
generalize to handle any prover (not just E)
2010-10-27, by blanchet
merged
2010-10-27, by huffman
make domain package work with non-cpo argument types
2010-10-27, by huffman
make op -->> infixr, to match op --->
2010-10-27, by huffman
use Named_Thms instead of Theory_Data for some domain package theorems
2010-10-26, by huffman
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
2010-10-26, by huffman
use Term.add_tfreesT
2010-10-26, by huffman
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
2010-10-24, by huffman
rename constant 'one_when' to 'one_case'
2010-10-24, by huffman
merged
2010-10-27, by haftmann
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
2010-10-27, by haftmann
regenerated keyword file
2010-10-27, by krauss
made SML/NJ happy
2010-10-27, by boehmes
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
2010-10-26, by blanchet
better list of irrelevant SMT constants
2010-10-26, by blanchet
if "debug" is on, print list of relevant facts (poweruser request);
2010-10-26, by blanchet
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26, by blanchet
"Nitpick" -> "Sledgehammer";
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
remove needless context argument;
2010-10-26, by blanchet
use proper context
2010-10-26, by boehmes
trace assumptions before giving them to the SMT solver
2010-10-26, by boehmes
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
2010-10-26, by boehmes
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
2010-10-26, by boehmes
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
2010-10-26, by haftmann
fixed typo
2010-10-26, by krauss
merged
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts
2010-10-26, by haftmann
more general treatment of type argument in code certificates for operations on abstract types
2010-10-26, by haftmann
partial_function is a declaration command
2010-10-26, by haftmann
merged
2010-10-26, by blanchet
proper error handling for SMT solvers in Sledgehammer
2010-10-26, by blanchet
NEWS
2010-10-26, by krauss
merge
2010-10-26, by blanchet
integrated "smt" proof method with Sledgehammer
2010-10-26, by blanchet
fixed confusion introduced in 008dc2d2c395
2010-10-26, by krauss
merged
2010-10-26, by blanchet
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
tuned
2010-10-26, by haftmann
merged
2010-10-26, by krauss
use partial_function instead of MREC combinator; curried rev'
2010-10-26, by krauss
added Heap monad instance of partial_function package
2010-10-26, by krauss
added Spec_Rule declaration to partial_function
2010-10-26, by krauss
basic documentation for command partial_function
2010-10-26, by krauss
remove outdated "(otherwise)" syntax from manual
2010-10-26, by krauss
declare recursive equation as ".simps", in accordance with other packages
2010-10-26, by krauss
merged
2010-10-26, by haftmann
dropped accidental doubled computation
2010-10-26, by haftmann
optionally force the remote version of an SMT solver to be executed
2010-10-26, by boehmes
tuned
2010-10-26, by boehmes
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
2010-10-26, by boehmes
changed SMT configuration options; updated SMT certificates
2010-10-26, by boehmes
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-26, by boehmes
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
2010-10-26, by boehmes
merged
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
clearer error messages
2010-10-26, by blanchet
renaming
2010-10-26, by blanchet
back again to non-Apple font rendering (cf. 4977324373f2);
2010-10-28, by wenzelm
dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible;
2010-10-28, by wenzelm
disable broken popups for now;
2010-10-26, by wenzelm
tuned;
2010-10-26, by wenzelm
do not handle arbitrary exceptions;
2010-10-26, by wenzelm
merged
2010-10-26, by wenzelm
Code_Runtime.trace
2010-10-26, by haftmann
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
2010-10-26, by wenzelm
merged
2010-10-26, by wenzelm
improved English
2010-10-26, by blanchet
whitespace tuning
2010-10-26, by blanchet
no need to encode theorem number twice in skolem names
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
make SML/NJ happy
2010-10-26, by blanchet
relaxing the filtering condition for getting specifications from Spec_Rules
2010-10-25, by bulwahn
adding new predicate compiler files to the IsaMakefile
2010-10-25, by bulwahn
using mode_eq instead of op = for lookup in the predicate compiler
2010-10-25, by bulwahn
renaming split_modeT' to split_modeT
2010-10-25, by bulwahn
options as first argument to check functions
2010-10-25, by bulwahn
changing test parameters in examples to get to a result within the global timelimit
2010-10-25, by bulwahn
adding a global fixed timeout to quickcheck
2010-10-25, by bulwahn
adding a global time limit to the values command
2010-10-25, by bulwahn
explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
2010-10-25, by wenzelm
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25, by wenzelm
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-25, by wenzelm
explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-10-25, by wenzelm
export main ML entry by default;
2010-10-25, by wenzelm
observe Isabelle/ML coding standards;
2010-10-25, by wenzelm
merged
2010-10-25, by wenzelm
significantly improved Isabelle/Isar implementation manual;
2010-10-25, by wenzelm
misc tuning;
2010-10-25, by wenzelm
removed some remains of Output.debug (follow-up to fce2202892c4);
2010-10-25, by wenzelm
recovered some odd two-dimensional layout;
2010-10-25, by wenzelm
merged
2010-10-25, by haftmann
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-25, by haftmann
moved sledgehammer to Plain; tuned dependencies
2010-10-25, by haftmann
CONTRIBUTORS
2010-10-25, by haftmann
merge
2010-10-25, by blanchet
merged
2010-10-25, by blanchet
updated keywords
2010-10-25, by blanchet
introduced manual version of "Auto Solve" as "solve_direct"
2010-10-25, by blanchet
make "sledgehammer_params" work on single-threaded platforms
2010-10-25, by blanchet
tuning
2010-10-22, by blanchet
handle timeouts (to prevent failure from other threads);
2010-10-22, by blanchet
update keywords
2010-10-25, by haftmann
some partial_function examples
2010-10-25, by krauss
added ML antiquotation @{assert};
2010-10-25, by wenzelm
updated keywords;
2010-10-25, by wenzelm
integrated partial_function into HOL-Plain
2010-10-23, by krauss
first version of partial_function package
2010-10-23, by krauss
Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem
2010-10-23, by krauss
merged
2010-10-25, by bulwahn
splitting Hotel Key card example into specification and the two tests for counter example generation
2010-10-22, by bulwahn
adding generator quickcheck
2010-10-22, by bulwahn
restructuring values command and adding generator compilation
2010-10-22, by bulwahn
moving general functions from core_data to predicate_compile_aux
2010-10-22, by bulwahn
updating to new notation in commented examples
2010-10-22, by bulwahn
merged
2010-10-24, by huffman
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
2010-10-24, by huffman
remove legacy comp_dbind option from domain package
2010-10-23, by huffman
change fixrec parser to not accept theorem names with (unchecked) option
2010-10-23, by huffman
tuned
2010-10-23, by huffman
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
2010-10-22, by huffman
add lemma strict3
2010-10-22, by huffman
do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas
2010-10-22, by huffman
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
2010-10-22, by huffman
direct instantiation unit :: discrete_cpo
2010-10-22, by huffman
remove finite_po class
2010-10-22, by huffman
simplify proofs about flift; remove unneeded lemmas
2010-10-22, by huffman
simplify proof
2010-10-22, by huffman
minimize imports
2010-10-21, by huffman
add type annotation to avoid warning
2010-10-21, by huffman
simplify some proofs, convert to Isar style
2010-10-21, by huffman
rename lemma spair_lemma to spair_Sprod
2010-10-21, by huffman
pcpodef (open) 'a lift
2010-10-21, by huffman
remove intro! attribute from {sinl,sinr}_defined
2010-10-21, by huffman
simplify proofs of ssumE, sprodE
2010-10-21, by huffman
merged
2010-10-24, by wenzelm
renamed nat_number
2010-10-24, by nipkow
nat_number -> eval_nat_numeral
2010-10-24, by nipkow
some cleanup in Function_Lib
2010-10-22, by krauss
merged
2010-10-22, by blanchet
compile
2010-10-22, by blanchet
added SMT solver to Sledgehammer docs
2010-10-22, by blanchet
more robust handling of "remote_" vs. non-"remote_" provers
2010-10-22, by blanchet
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
2010-10-22, by blanchet
replaced references with proper record that's threaded through
2010-10-22, by blanchet
fixed signature of "is_smt_solver_installed";
2010-10-22, by blanchet
renamed modules
2010-10-22, by blanchet
renamed files
2010-10-22, by blanchet
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
2010-10-22, by blanchet
remove more needless code ("run_smt_solvers");
2010-10-22, by blanchet
got rid of duplicate functionality ("run_smt_solver_somehow");
2010-10-22, by blanchet
bring ATPs and SMT solvers more in line with each other
2010-10-22, by blanchet
make Sledgehammer minimizer fully work with SMT
2010-10-22, by blanchet
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
2010-10-22, by blanchet
first step in adding support for an SMT backend to Sledgehammer
2010-10-21, by blanchet
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-10-21, by blanchet
cosmetics
2010-10-21, by blanchet
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
2010-10-22, by krauss
Changed section title to please LaTeX.
2010-10-22, by hoelzl
temporary removed Predicate_Compile_Quickcheck_Examples from tests
2010-10-21, by bulwahn
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-10-21, by bulwahn
using a signature in core_data and moving some more functions to core_data
2010-10-21, by bulwahn
splitting large core file into core_data, mode_inference and predicate_compile_proof
2010-10-21, by bulwahn
added generator_dseq compilation for a sound depth-limited compilation with small value generators
2010-10-21, by bulwahn
for now safely but unpractically assume no predicate is terminating
2010-10-21, by bulwahn
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
2010-10-21, by bulwahn
adding option smart_depth_limiting to predicate compiler
2010-10-21, by bulwahn
merged
2010-10-20, by huffman
introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
2010-10-20, by huffman
add lemma lub_eq_bottom_iff
2010-10-20, by huffman
combine check_and_sort_domain with main function; rewrite much of the error-checking code
2010-10-20, by huffman
constructor arguments with selectors must have pointed types
2010-10-20, by huffman
simplify check_and_sort_domain; more meaningful variable names
2010-10-20, by huffman
replace fixrec 'permissive' mode with per-equation 'unchecked' option
2010-10-19, by huffman
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
2010-10-19, by huffman
simplify some proofs; remove some unused lists of lemmas
2010-10-19, by huffman
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
2010-10-19, by huffman
eliminate constant 'coerce'; use 'prj oo emb' instead
2010-10-19, by huffman
simplify fixrec pattern match function
2010-10-19, by huffman
simplify some proofs
2010-10-17, by huffman
tuned
2010-10-19, by Christian Urban
added some facts about factorial and dvd, div and mod
2010-10-19, by bulwahn
removing something that probably slipped into the Quotient_List theory
2010-10-19, by bulwahn
Quotient package: partial equivalence introduction
2010-10-19, by Cezary Kaliszyk
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
2010-10-18, by Christian Urban
remove dead code
2010-10-16, by huffman
remove old uses of 'simp_tac HOLCF_ss'
2010-10-16, by huffman
merged
2010-10-16, by huffman
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
2010-10-16, by huffman
reimplement proof automation for coinduct rules
2010-10-16, by huffman
add functions mk_imp, mk_all
2010-10-16, by huffman
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
2010-10-15, by huffman
simplify automation of induct proof
2010-10-15, by huffman
add function mk_adm
2010-10-15, by huffman
rewrite proof automation for finite_ind; get rid of case_UU_tac
2010-10-15, by huffman
put constructor argument specs in constr_info type
2010-10-14, by huffman
avoid using Global_Theory.get_thm
2010-10-14, by huffman
include iso_info as part of constr_info type
2010-10-14, by huffman
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
2010-10-14, by huffman
add take_strict_thms field to take_info type
2010-10-14, by huffman
add record type synonym 'constr_info'
2010-10-14, by huffman
add function take_theorems
2010-10-14, by huffman
add type annotation to avoid warning
2010-10-14, by huffman
cleaned up Fun_Cpo.thy; deprecated a few theorem names
2010-10-13, by huffman
edit comments
2010-10-13, by huffman
remove unneeded lemmas Lift_exhaust, Lift_cases
2010-10-12, by huffman
move lemmas from Lift.thy to Cfun.thy
2010-10-12, by huffman
cleaned up Adm.thy
2010-10-12, by huffman
remove unneeded lemmas from Fun_Cpo.thy
2010-10-12, by huffman
remove unused lemmas
2010-10-12, by huffman
reformulate lemma cont2cont_lub and move to Cont.thy
2010-10-12, by huffman
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
2010-10-12, by huffman
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
2010-10-11, by huffman
rename Ffun.thy to Fun_Cpo.thy
2010-10-11, by huffman
remove unused constant 'directed'
2010-10-11, by huffman
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
2010-10-11, by huffman
merged
2010-10-15, by paulson
prevention of self-referential type environments
2010-10-15, by paulson
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
2010-10-15, by Cezary Kaliszyk
FSet tuned
2010-10-15, by Cezary Kaliszyk
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
2010-10-15, by Cezary Kaliszyk
NEWS
2010-10-14, by krauss
removed output syntax "'a ~=> 'b" for "'a => 'b option"
2010-10-10, by krauss
reactivated
2010-10-13, by krauss
slightly more robust proof
2010-10-12, by krauss
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
2010-10-11, by huffman
merged
2010-10-11, by huffman
move all bifinite class instances to Bifinite.thy
2010-10-09, by huffman
rename class 'sfp' to 'bifinite'
2010-10-08, by huffman
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
2010-10-07, by huffman
add lemma typedef_ideal_completion
2010-10-07, by huffman
remove unused lemmas
2010-10-07, by huffman
remove Infinite_Set from ROOT.ML
2010-10-07, by huffman