tuning

pass certain readability-enhancing Vampire options only when an Isar proof is needed

added lemma

added lemma

renamings

code tuning

signature tuning

removed dead code

tuned signature

store (co)induction rules in data structure

tuning names

got rid of needless library function (find_minimum)

one more lib function

export one more function

rationalized data structure

added and moved library functions (used in primrec code)

tuned names -- co_ and un_ with underscore are to be understood as (co) and (un)

tuning

more code rationalization

more code rationalization

more code rationalization

refactoring

tuned

renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries

tuned

tuned

tuning

export more functions (useful for primrec_new)

further enrich data structure

more

rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)

added fields to database

tuned data structure

renamed records

added constructors to data structure

added pre-BNFs to database

lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)

renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)

Added maps, sets, rels to "simps" thm collection

tuned

comment tuning

tuning

tuning

tuning

signature tuning

whitespace tuning

tuned signature

canonical names of classes

merged

register all (co)datatypes in local data

create data structure for storing (co)datatype information

avoid empty isabelletags.sty for the sake of arXiv;

merged

cygwin_root as optional argument; tuned;

use record instead of big tuple

clarified module dependencies: avoid Properties and Document introding minimal "PIDE";

merge

use base names, not full names

tune signatures

tuning

tuning

removed unreferenced thm

tuned function signatures

factored out derivation of coinduction, unfold, corec

code tuning

factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual

tuned

tuned operator precedence

use record instead of huge tuple

renamed BNF "(co)data" commands to names that are closer to their final names

tuned

tuned

tuned

tuned

Clarified confusing sentence in locales tutorial.

uniform Proof.context for hyp_subst_tac;

tuned ML and thy file names

merged

for compatibility, generate recursor arguments in the same order as old package

tuning in preparation for actual changes

started working on compatibility with old package's recursor

simplified def

more standard argument order

more intuitive syntax for equality-style discriminators of nullary constructors

updated keywords

put an underscore in prefix

changed discriminator default: avoid mixing ctor and dtor views

simplified def

more standard order of arguments

more funs

simplified def

removed unnecessary assumptions in some theorems about cardinal exponentiation

renamed "wrap_data" to "wrap_free_constructors"

register coinductive type's coinduct rule

compile

adjusted stream library to coinduct attributes

generate proper attributes for coinduction rules

updated to jdk-7u21;

revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space

renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)

spell conditional_ly_-complete lattices correct

specify nicer names for map, set and rel in the stream library

start making "wrap_data" more robust

no eta-expansion for case in split rules and case_conv

simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)

proper error generated for wrong mixfix

honor user-specified name for relator + generalize syntax

renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus

added "fundef_cong" attribute to "map_cong"

optimized proofs

apply arguments to f and g in "case_cong"

derive "map_cong"

renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"

killed dead code

eta-contracted weak congruence rules (like in the old package)

honor user-specified name for map function

honor user-specified set function names

parse set function name

merged

tuned

took out workaround for bug fixed in 5af40820948b

merged

slightly more aggressive syntax translation for printing case expressions

avoid odd reinit after sublocale declaration

moved defs into locale to reduce unnecessary polymorphism; tuned

dropped dead code

documentation and NEWS

avoid accidental specialization of the types in the "map" property of codatatypes

simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)

more examples

tuning

fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)

tuning

tuned_comment

(co)rec is (just as the (un)fold) the unique morphism;

tuned: unnamed contexts, interpretation and sublocale in locale target; corrected slip in List.thy: setsum requires commmutativity

target-sensitive user-level commands interpretation and sublocale

ML interfaces for various kinds of interpretation

brittleness stamping for local theories

tuned

removed type constraints

NEWS

more sharing

interpretation: distinguish theories and proofs by explicit parameter rather than generic context; formal initialisation of theory target during interpretation; prefer Local_Theory.notes_kind to register mixin equations during interpretation; more uniformity between note_eqns_register and note_eqns_dependency

dropped unusued identifier

avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target

tuned for uniformity

reflection as official HOL tool

follow Isabelle spacing praxis more thoroughly

honour FIXMEs as far as feasible at the moment

combined reify_data.ML into reflection.ML; attempt to establish a more accessible and more consistent terminology; more ML code in ML file rather than setup theory; ML slightly tuned wrt. Isabelle coding conventions

proved termination for fun-based AI

tuned

tuned

merged

tuned signature;

simplifier uses proper Proof.context instead of historic type simpset;

merged

avoided map_of in def of fun_rep (but still needed for efficient code)

spelling

spelling

tuned

complete revision: finally got rid of annoying L-predicate

moved leastness lemma

proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2); speculative update for yap (untested);

use automatic type coerctions in Sqrt example

make SML/NJ happy;

not all Nitpick 'constructors' are injective -- careful

added another definition snipped

actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;

modifiers for classical wrappers operate on Proof.context instead of claset;

removed historic comments;

tuned exceptions -- avoid composing error messages in low-level situations;

tuned signature; tuned comments;

proper identifiers -- avoid crash of case translations;

reduced duplication

do not add case translation syntax in rep_datatype compatibility mode

run type inference on input to wrap_data

installed case translations in BNF package

tuned

more antiquotations;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;

updated keywords;

merged

merged

obsolete -- tools should refer to proper Proof.context;

discontinued obsolete ML antiquotation @{claset};

added ML antiquotation @{theory_context};

more standard module name Axclass (according to file name);

made SML/NJ happy

generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector

NEWS and CONTRIBUTORS