isabelle: Graph

merged
2010-10-29, by wenzelm
added user aliasses (still unclear how to specify names with whitespace contained)
2010-10-29, by haftmann
merged
2010-10-29, by haftmann
tuned structure of theory
2010-10-29, by haftmann
remove term_of equations for Heap type explicitly
2010-10-29, by haftmann
no need for setting up the kodkodi environment since Kodkodi 1.2.9
2010-10-29, by blanchet
fixed order of quantifier instantiation in new Skolemizer
2010-10-29, by blanchet
restructure Skolemization code slightly
2010-10-29, by blanchet
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
2010-10-29, by blanchet
more work on new Skolemizer without Hilbert_Choice
2010-10-29, by blanchet
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
2010-10-29, by blanchet
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
2010-10-29, by blanchet
make handling of parameters more robust, by querying the goal
2010-10-29, by blanchet
actually pass "verbose" argument
2010-10-29, by haftmann
eliminated obsolete \_ escape;
2010-10-29, by wenzelm
eliminated obsolete \_ escapes in rail environments;
2010-10-29, by wenzelm
proper markup of formal text;
2010-10-29, by wenzelm
merged
2010-10-29, by wenzelm
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
2010-10-29, by krauss
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
2010-10-29, by blanchet
merged
2010-10-29, by Lars Noschinski
Remove unnecessary premise of mult1_union
2010-09-22, by Lars Noschinski
adapting HOL-Mutabelle to changes in quickcheck
2010-10-29, by bulwahn
NEWS
2010-10-29, by bulwahn
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
2010-10-29, by bulwahn
updating documentation on quickcheck in the Isar reference
2010-10-29, by bulwahn
merged
2010-10-28, by bulwahn
adding a simple check to only run with a SWI-Prolog version known to work
2010-10-28, by bulwahn
tuned messages;
2010-10-28, by wenzelm
discontinued obsolete ML antiquotation @{theory_ref};
2010-10-28, by wenzelm
tuned;
2010-10-28, by wenzelm
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
2010-10-28, by wenzelm
type attribute is derived concept outside the kernel;
2010-10-28, by wenzelm
preserve original source position of exn;
2010-10-28, by wenzelm
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
2010-10-28, by wenzelm
use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
2010-10-28, by wenzelm
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
2010-10-28, by wenzelm
eliminated dead code;
2010-10-28, by wenzelm
tuned white-space;
2010-10-28, by wenzelm
merged
2010-10-28, by nipkow
added lemmas about listrel(1)
2010-10-28, by nipkow
tuned;
2010-10-28, by wenzelm
merged
2010-10-28, by wenzelm
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
2010-10-28, by blanchet
merged
2010-10-28, by blanchet
clear identification
2010-10-28, by blanchet
clear identification;
2010-10-28, by blanchet
clear identification
2010-10-28, by blanchet
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
2010-10-27, by blanchet
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
remove some junk that made it in by accient
2010-10-07, by huffman
"setup" in theory
2010-10-11, by blanchet
added "trace_meson" configuration option, replacing old-fashioned reference
2010-10-11, by blanchet
added "trace_metis" configuration option, replacing old-fashioned references
2010-10-11, by blanchet
do not mention unqualified names, now that 'global' and 'local' are gone
2010-10-10, by krauss
simplified proof
2010-10-10, by nipkow
avoid generating several formulas with the same name ("tfrees")
2010-10-10, by blanchet
major reorganization/simplification of HOLCF type classes:
2010-10-06, by huffman
add lemma finite_deflation_intro
2010-10-05, by Brian Huffman
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
2010-10-05, by Brian Huffman
move lemmas to Deflation.thy
2010-10-05, by Brian Huffman
simplify proofs of powerdomain inequalities
2010-10-05, by Brian Huffman
new lemmas about lub
2010-10-04, by huffman
define is_ub predicate using bounded quantifier
2010-10-04, by huffman
minimize theory imports
2010-10-02, by huffman
added lemmas to List_Cpo.thy
2010-10-01, by huffman
new_domain emits proper error message when a constructor argument type does not have sort 'rep'
2010-09-30, by huffman
move code from "Metis_Tactics" to "Metis_Reconstruct"
2010-10-06, by blanchet
merged
2010-10-06, by blanchet
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
2010-10-06, by blanchet
get rid of function that duplicates existing Pure functionality
2010-10-06, by blanchet
remove needless fact
2010-10-06, by blanchet
added a few FIXMEs
2010-10-06, by blanchet
tuned comments
2010-10-05, by blanchet
document latest changes to Meson/Metis/Sledgehammer
2010-10-05, by blanchet
remove needless Metis facts
2010-10-05, by blanchet
hide one more name
2010-10-05, by blanchet
qualify names
2010-10-05, by blanchet
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
2010-10-05, by blanchet
clean up debugging output
2010-10-05, by blanchet
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
2010-10-05, by blanchet
got rid of overkill "meson_choice" attribute;
2010-10-05, by blanchet
more explicit name
2010-10-05, by blanchet
factor out "Meson_Tactic" from "Meson_Clausify"
2010-10-05, by blanchet
tuning
2010-10-04, by blanchet
move Metis into Plain
2010-10-04, by blanchet
added "Meson" theory to Makefile
2010-10-04, by blanchet
update authors
2010-10-04, by blanchet
remove Meson from Hilbert_Choice
2010-10-04, by blanchet
remove Meson from Sledgehammer
2010-10-04, by blanchet
move Meson to Plain
2010-10-04, by blanchet
move MESON files together
2010-10-04, by blanchet
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
2010-10-04, by blanchet
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
2010-10-04, by blanchet
correctly handle multiple copies of the same axiom with the same types
2010-10-04, by blanchet
put two operations in the right order
2010-10-04, by blanchet
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
2010-10-04, by blanchet
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
2010-10-04, by blanchet
instantiate foralls and release exists in the order described by the topological order
2010-10-04, by blanchet
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
2010-10-04, by blanchet
renamed internal function
2010-10-04, by blanchet
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
2010-10-04, by blanchet
tuned header
2010-10-06, by haftmann
tuned
2010-10-05, by krauss
force less agressively
2010-10-05, by krauss
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
2010-10-05, by krauss
removed complicated (and rarely helpful) error reporting
2010-10-05, by krauss
discontinued continuations to simplify control flow; dropped optimization in scnp
2010-10-05, by krauss
use Cache structure instead of passing tables around explicitly
2010-10-05, by krauss
merged
2010-10-05, by haftmann
lemmas fold_commute and fold_commute_apply
2010-10-05, by haftmann
spelling
2010-05-07, by krauss
adjusted to inductive characterization of sorted
2010-10-04, by haftmann
tuned whitespace
2010-10-04, by haftmann
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-10-04, by haftmann
turned distinct and sorted into inductive predicates: yields nice induction principles for free
2010-10-04, by haftmann
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-10-04, by haftmann
some Poly/ML-specific debugging code escaped in the wild -- comment it out
2010-10-02, by blanchet
merged
2010-10-01, by haftmann
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
2010-10-01, by haftmann
moved ML_Context.value to Code_Runtime
2010-10-01, by haftmann
constant `contents` renamed to `the_elem`
2010-10-01, by haftmann
merged
2010-10-01, by blanchet
tune whitespace
2010-10-01, by blanchet
rename bound variables after skolemizing, if the axiom of choice is available
2010-10-01, by blanchet
tuning
2010-10-01, by blanchet
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
2010-10-01, by blanchet
tune bound names
2010-10-01, by blanchet
merged
2010-10-01, by blanchet
avoid dependency on "int"
2010-10-01, by blanchet
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
2010-10-01, by blanchet
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
2010-10-01, by blanchet
compute quantifier dependency graph in new skolemizer
2010-10-01, by blanchet
tuning
2010-10-01, by blanchet
compute substitutions in new skolemizer
2010-10-01, by blanchet
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
2010-09-30, by blanchet
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
2010-09-30, by blanchet
encode number of skolem assumptions in them, for more efficient retrieval later
2010-09-30, by blanchet
move functions closer to where they're used
2010-09-30, by blanchet
Skolemizer tweaking
2010-09-30, by blanchet
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
2010-09-29, by blanchet
finished renaming file and module
2010-09-29, by blanchet
rename file
2010-09-29, by blanchet
ignore Skolem assumption (if any)
2010-09-29, by blanchet
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
2010-09-29, by blanchet
first step towards a new skolemizer that doesn't require "Eps"
2010-09-29, by blanchet
cumulative update of generated files (since bf164c153d10);
2010-10-22, by wenzelm
removed ML_old.thy, which is largely superseded by ML.thy;
2010-10-22, by wenzelm
more on "Canonical argument order";
2010-10-22, by wenzelm
cover @{Isar.state};
2010-10-22, by wenzelm
more on "Style and orthography";
2010-10-22, by wenzelm
more on "Naming conventions";
2010-10-22, by wenzelm
tuned;
2010-10-22, by wenzelm
more on "Style and orthography";
2010-10-21, by wenzelm
more refs;
2010-10-21, by wenzelm
preliminary material on "Concrete syntax and type-checking";
2010-10-21, by wenzelm
more on "Association lists", based on more succinct version of older material;
2010-10-20, by wenzelm
clarified "lists as a set-like container";
2010-10-20, by wenzelm
more robust treatment of "op IDENT";
2010-10-19, by wenzelm
more on messages;
2010-10-19, by wenzelm
more on synchronized variables;
2010-10-19, by wenzelm
tuned;
2010-10-19, by wenzelm
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
2010-10-19, by wenzelm
misc tuning;
2010-10-19, by wenzelm
somewhat modernized version of "Thread-safe programming";
2010-10-18, by wenzelm
more robust examples: explicit @{assert} instead of unchecked output;
2010-10-18, by wenzelm
more on "Configuration options";
2010-10-18, by wenzelm
tuned;
2010-10-18, by wenzelm
more on "Basic data types";
2010-10-18, by wenzelm
more on "Integers";
2010-10-17, by wenzelm
use continental paragraph style, which works better with mixture of (in)formal text;
2010-10-17, by wenzelm
robustified "warn" environment if \parindent is zero (e.g. within itemize, description etc.);
2010-10-17, by wenzelm
more on "Basic ML data types";
2010-10-16, by wenzelm
more robust treatment of symbolic indentifiers (which may contain colons);
2010-10-16, by wenzelm
more examples;
2010-10-16, by wenzelm
tuned;
2010-10-16, by wenzelm
more on "Exceptions";
2010-10-16, by wenzelm
more on "Exceptions";
2010-10-15, by wenzelm
more examples;
2010-10-15, by wenzelm
tuned chapter arrangement;
2010-10-15, by wenzelm
more examples;
2010-10-15, by wenzelm
moved bind_thm(s) to implementation manual;
2010-10-15, by wenzelm
more on "Attributes";
2010-10-14, by wenzelm
misc tuning and clarification;
2010-10-14, by wenzelm
more on "Proof methods";
2010-10-13, by wenzelm
examples in Isabelle/HOL;
2010-10-13, by wenzelm
more on Proof.theorem;
2010-10-13, by wenzelm
tuned;
2010-10-13, by wenzelm
more examples;
2010-10-12, by wenzelm
more on "Isar language elements";
2010-10-12, by wenzelm
more examples;
2010-10-11, by wenzelm
more refs;
2010-10-11, by wenzelm
misc tuning;
2010-10-11, by wenzelm
removed some obsolete reference material;
2010-10-10, by wenzelm
cover some more theory operations;
2010-10-10, by wenzelm
note on Isabelle file specifications;
2010-10-10, by wenzelm
modernized version of "Message output channels";
2010-10-10, by wenzelm
removed some really old reference material;
2010-10-10, by wenzelm
more examples;
2010-10-09, by wenzelm
various concrete ML antiquotations;
2010-10-09, by wenzelm
prefer checked antiquotations;
2010-10-09, by wenzelm
clarified tag markup;
2010-10-09, by wenzelm
more on ML antiquotations;
2010-10-08, by wenzelm
keep normal size for %mlref tag;
2010-10-08, by wenzelm
basic setup for ML antiquotations -- with rail diagrams;
2010-10-08, by wenzelm
eliminated "Toplevel control", which belongs to TTY/ProofGeneral model;
2010-10-08, by wenzelm
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
2010-10-08, by wenzelm
misc tuning;
2010-10-08, by wenzelm
more on Isabelle/ML;
2010-10-07, by wenzelm
basic setup for Chapter 0: Isabelle/ML;
2010-10-07, by wenzelm
minor tuning and updating;
2010-10-07, by wenzelm
made SML/NJ happy;
2010-10-01, by wenzelm
merged
2010-10-01, by wenzelm
use module integer for Eval
2010-10-01, by haftmann
check whole target hierarchy for existing reserved symbols
2010-10-01, by haftmann
added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
2010-10-01, by haftmann
tuned default "Prover Session" perspective;
2010-10-01, by wenzelm
eliminated ancient OldTerm.term_frees;
2010-10-01, by wenzelm
more antiquotations;
2010-10-01, by wenzelm
simplified outer syntax setup;
2010-10-01, by wenzelm
chop_while replace drop_while and take_while
2010-10-01, by haftmann
merged
2010-10-01, by haftmann
take_while, drop_while
2010-09-30, by haftmann
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
2010-09-30, by huffman
fixrec: rename match_cpair to match_Pair
2010-09-30, by huffman
remove code for obsolete 'fixpat' command
2010-09-15, by huffman
clean up definition of compile_pat function
2010-09-15, by huffman
rename some fixrec pattern-match compilation functions
2010-09-15, by huffman
adding example for case expressions
2010-09-30, by bulwahn
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
2010-09-30, by bulwahn
merged
2010-09-30, by bulwahn
adapting manual configuration in examples
2010-09-30, by bulwahn
finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)
2010-09-30, by bulwahn
adding option to globally limit the prolog execution
2010-09-30, by bulwahn
removing dead code
2010-09-30, by bulwahn
value uses bare compiler invocation: generated code does not contain antiquotations
2010-09-30, by haftmann
updated files to recent changes
2010-09-30, by haftmann
corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity
2010-09-30, by haftmann
tuned
2010-09-30, by haftmann
merged
2010-09-30, by haftmann
redundancy check: drop trailing Var arguments (avoids eta problems with equations)
2010-09-29, by haftmann