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'

move code from "Metis_Tactics" to "Metis_Reconstruct"

merged

qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)

get rid of function that duplicates existing Pure functionality

remove needless fact

added a few FIXMEs

tuned comments

document latest changes to Meson/Metis/Sledgehammer

remove needless Metis facts

hide one more name

qualify names

hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names

clean up debugging output

factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure

got rid of overkill "meson_choice" attribute; tuning

more explicit name

factor out "Meson_Tactic" from "Meson_Clausify"

tuning

move Metis into Plain

added "Meson" theory to Makefile

update authors

remove Meson from Hilbert_Choice

remove Meson from Sledgehammer

move Meson to Plain

move MESON files together

paramify new skolems just like old ones (cf. reveal_old_skolem_terms)

fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset

correctly handle multiple copies of the same axiom with the same types

put two operations in the right order

reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism

apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed

instantiate foralls and release exists in the order described by the topological order

reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables

renamed internal function

hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving

tuned header

tuned

force less agressively

lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed

removed complicated (and rarely helpful) error reporting

discontinued continuations to simplify control flow; dropped optimization in scnp

use Cache structure instead of passing tables around explicitly

merged