simplify some proofs, convert to Isar style

rename lemma spair_lemma to spair_Sprod

pcpodef (open) 'a lift

remove intro! attribute from {sinl,sinr}_defined

simplify proofs of ssumE, sprodE

merged

renamed nat_number

nat_number -> eval_nat_numeral

some cleanup in Function_Lib

merged

compile

added SMT solver to Sledgehammer docs

more robust handling of "remote_" vs. non-"remote_" provers

generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)

replaced references with proper record that's threaded through

fixed signature of "is_smt_solver_installed"; renaming

renamed modules

renamed files

took out "smt"/"remote_smt" from default ATPs until they are properly implemented

remove more needless code ("run_smt_solvers"); tuning

got rid of duplicate functionality ("run_smt_solver_somehow"); added minimization command to SMT solver message

bring ATPs and SMT solvers more in line with each other

make Sledgehammer minimizer fully work with SMT

generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well

first step in adding support for an SMT backend to Sledgehammer

use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."

cosmetics

relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version

Changed section title to please LaTeX.

temporary removed Predicate_Compile_Quickcheck_Examples from tests

adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog

using a signature in core_data and moving some more functions to core_data

splitting large core file into core_data, mode_inference and predicate_compile_proof

added generator_dseq compilation for a sound depth-limited compilation with small value generators

for now safely but unpractically assume no predicate is terminating

adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible

adding option smart_depth_limiting to predicate compiler

merged

introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions

add lemma lub_eq_bottom_iff

combine check_and_sort_domain with main function; rewrite much of the error-checking code

constructor arguments with selectors must have pointed types

simplify check_and_sort_domain; more meaningful variable names

replace fixrec 'permissive' mode with per-equation 'unchecked' option

rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML

simplify some proofs; remove some unused lists of lemmas

replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function

eliminate constant 'coerce'; use 'prj oo emb' instead

simplify fixrec pattern match function

simplify some proofs

tuned

added some facts about factorial and dvd, div and mod

removing something that probably slipped into the Quotient_List theory

Quotient package: partial equivalence introduction

reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)

remove dead code

remove old uses of 'simp_tac HOLCF_ss'

merged

remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check

reimplement proof automation for coinduct rules

add functions mk_imp, mk_all

move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code

simplify automation of induct proof

add function mk_adm

rewrite proof automation for finite_ind; get rid of case_UU_tac

put constructor argument specs in constr_info type

avoid using Global_Theory.get_thm

include iso_info as part of constr_info type

remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors

add take_strict_thms field to take_info type

add record type synonym 'constr_info'

add function take_theorems

add type annotation to avoid warning

cleaned up Fun_Cpo.thy; deprecated a few theorem names

edit comments

remove unneeded lemmas Lift_exhaust, Lift_cases

move lemmas from Lift.thy to Cfun.thy

cleaned up Adm.thy

remove unneeded lemmas from Fun_Cpo.thy

remove unused lemmas

reformulate lemma cont2cont_lub and move to Cont.thy

remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2

new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI

rename Ffun.thy to Fun_Cpo.thy

remove unused constant 'directed'

add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite

merged

prevention of self-referential type environments

FSet: definition changes propagated from Nominal and more use of 'descending' tactic

FSet tuned

FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash

NEWS

removed output syntax "'a ~=> 'b" for "'a => 'b option"

reactivated

slightly more robust proof

renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)

merged

move all bifinite class instances to Bifinite.thy

rename class 'sfp' to 'bifinite'

move stuff from Algebraic.thy to Bifinite.thy and elsewhere

add lemma typedef_ideal_completion

remove unused lemmas

remove Infinite_Set from ROOT.ML

remove some junk that made it in by accient

"setup" in theory

added "trace_meson" configuration option, replacing old-fashioned reference

added "trace_metis" configuration option, replacing old-fashioned references

do not mention unqualified names, now that 'global' and 'local' are gone

simplified proof

avoid generating several formulas with the same name ("tfrees")

major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);

add lemma finite_deflation_intro

add lemmas finite_deflation_imp_compact, cast_below_cast_iff

move lemmas to Deflation.thy

simplify proofs of powerdomain inequalities

new lemmas about lub

define is_ub predicate using bounded quantifier

minimize theory imports

added lemmas to List_Cpo.thy

new_domain emits proper error message when a constructor argument type does not have sort 'rep'