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