use theory data for REP_simps and isodefl_rules

replace defl_tab and map_tab with theory data

separate conjuncts of isodefl theorem

automate isodefl proof

change example to use recursion with continuous function space

add lemma isodefl_cprod

automate definition of map functions; remove unused code

change naming convention for deflation combinators

add new makefile dependencies

prove isomorphism and isodefl rules

avoid using csplit; define copy functions exactly like the current domain package

merged

remove one_typ and tr_typ; add abs/rep lemmas

automate definition of rep/abs functions

get rid of numbers on thy variables

automate proofs of REP equations

cleaned up; factored out fixed-point definition code

automate solution of domain equations

removed fixme - quick-and-dirty flag is appropriate

use of thm-antiquotation

Added new counterexample generator SML_inductive for goals involving inductive predicates.

Added infrastructure for embedding random data generators into code generated for inductive predicates.

unused_thms: show only results from 'theorem(s)' package (via old-style kinds); misc tuning -- slightly less hermetic names;

future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;

toplevel pretty printer for Synchronized.var;

adapted Local_Theory.define -- eliminated odd thm kind;

Specification.definition: Thm.definitionK marks exactly the high-level end-user result;

Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;

merged

merged

Minor correction

some attempts to improve termination of isatest;

Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS

Renamed vector_less_eq_def to the more usual name vector_le_def.

merged

replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules

concealing internal definitions of primrec specifications

adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler

changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler

adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned

check if equations are present for all functions to avoid low-level exception later

anti_sym -> antisym

optionally trace theorems used in proof reconstruction

added arithmetic example using div and mod

bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits; the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

merged

comment out debugging code in Nitpick

fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"

made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions

removed "debug := true" that shouldn't have been submitted in the first place

Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)

merged

run Nitpick examples if Kodkodi is available

merged

fixed "expect" of Nitpick examples to reflect latest changes in Nitpick

merged

use SAT solver that's available everywhere for this example

invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script; this requires downloading Kodkodi 1.2.4, or writing a "kodkodi" script that invokes "java de.tum.in.isabelle.Kodkodi.Kodkodi $@"

merged

added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus