qpaper / example interaction

Qpaper/regularization proof.

qpaper

Qpaper/more.

Qpaper/Minor

added larry's quote

added larry's paper

tuned

first version of the abstract

merged

fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set

qpaper / lemmas used in proofs

qpaper / injection statement

qpaper / regularize

qpaper / a bit about prs

Functionalized the ABS/REP definition.

qpaper / lifting introduction

merged

fixed compile error

qpaper / composition of quotients.

qpaper

qpaper..

qpaper.

Name some respectfullness

added FSet to the correct paper

merged

added FSet

qpaper

qpaper

Substitution Lemma for TypeSchemes.

Simplified the proof

A lemma about substitution in TypeSchemes.

reversing the direction of fresh_star

overlapping deep binders proof

edits from the reviewers

tuned paper

changed qpaper to lncs-style

Match_Lam defined on Quotient Level.

More on Function-defined subst.

Isabelle renamings

merge

Renamings.

Renamings

merge (non-trival)

Previously uncommited direct subst definition changes.

Function experiments

merged

added comments about pottiers work

more subst experiments

More subst experminets

more on subst

Single variable substitution

subst fix

subst experiments

soem minor tuning

Fix broken add

add missing .bib

merge

starting bibliography

merged

updated to new Isabelle (More_Conv -> Conv)

made this example to work again

merge

alpha_alphabn for bindings in a type under bn.

minor tuning

Ex4 does work, and I don't see the difference between the alphas.

slight tuning

somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms

moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat

tuned paper

tuned paper

tuned a bit the paper

started a new file for the parser to make some experiments

moved old parser and fv into attic

polished example

merged

tuned a bit the paper

Proper fv/alpha for multiple compound binders

SingleLetFoo with everything.

Fv for multiple binding functions

added a more instructive example - has some problems with fv though

added flip_eqvt and swap_eqvt to the equivariance lists

tuned the paper

properly declared outer keyword

added an example which goes outside our current speciifcation

made out of STEPS a configuration value so that it can be set individually in each file

tuned eqvt-proofs about prod_rel and prod_fv

removed internal functions from the signature (they are not needed anymore)

added term4 back to the examples

Make Term4 use 'equivariance'.

fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy

merged

moved the data-transformation into the parser

added a test whether some of the constants already equivariant (then the procedure has to fail).

include set_simps and append_simps in fv_rsp

Move alpha_eqvt to unused.

Use equivariance instead of alpha_eqvt

merge

merge

fvbv_rsp include prod_rel.simps

better ML-interface (returning only a list of theorems and a context)

merge

Use raw_induct instead of induct

ingnored parameters in equivariance; added a proper interface to be called from ML

properly exported defined bn-functions

Include raw permutation definitions in eqvt

Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'

a bit for the introduction of the q-paper

added some of the quotient literature; a bit more to the qpaper

fixed a problem with non-existant alphas2

added comment about bind_set

fixing bind_set problem

merge

Term8 comment

merge

Restore set bindings in CoreHaskell

Recursive examples with relation composition

merge

prod_rel and prod_fv eqvt and mono

ExLetRec