Fix Term4 for permutation signature change

Move LF to NewParser. Just works.

merge

ExLetMult

Ex1Rec.

merge

merge

ExPS3 in NewParser

Move ExPS8 to new parser.

Fix for new isabelle

merge

Minor

increased step counter so that all steps go through

fixed my error with define_raw_fv

tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function

Separate Term8, as it may work soon.

moved CoreHaskell to NewParser.

ExPS7 in NewParser

Move ExLeroy to New Parser

Move 2 more to NewParser

Move TypeSchemes to NewParser

Move ExLet to NewParser.

tuned

roll back of the last commit (there was a difference)

tuned

to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm

merged

some preliminary changes to the pearl-jv paper

some preliminary notes of the abstract (qpaper); still need to see the motivating example

Added cheats to classical

Ex2 moved to new parser.

alpha_eqvt_tac fixed to work when the existential is not at the top level.

SingleLet and Ex3 work with NewParser.

Comment

Another example where only alpha_eqvt fails.

Register only non-looping rules in eq_iff

Equivariance fails for single let?

NewParser

Introduce eq_iff_simp to match the one from Parser.

remove tracing

Cheat support equations in new parser

Remove dependency on NewFv

Fix Parser

Add explicit cheats in NewParser and comment out the examples for outside use.

Fix Datatype_Aux calls in NewParser.

Move old fv_alpha_export to Fv.

moved old parser and old fv back into their original places; isabelle make works again

slight tuning

simplified the supp-of-finite-sets proof

tried to add some comments in the huge(!) nominal2_cmd function

replaced make_pair with library function HOLogic.mk_prod

removed duplicate eqvt attribute

attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)

merged

tuned

replaced hide by the new hide_const

generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)

added lemmas establishing the support of finite sets of finitely supported elements

added eqvt-lemmas for Bex, Ball and Union

NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.

Merged nominal_datatype into NewParser until eqvts

more parser/new parser synchronization.

Simplify old parser for integration

merge

Change signature of fv and alpha generation.

reorganised eqvt-file (now uses perm_simp already)

qpaper

merge

New Alpha.

Minimal cleaning in LamEx

Remove things moved to the isabelle distribution

Unify and give only one name to 'setify', 'listify' and 'set'

Fixing the definitions in the Parser.

Some of the exceptions that the parser should check in TODO.

Extracting the fv body function and exporting the terms.

Fix for recursive binders.

revert 0c9ef14e9ba4

Support in positive position and atoms in negative positions.

merge

Include support of unknown datatypes in new fv

merged

added basic functions for constructing supp-terms

quotient paper

added missing latex-style file

merged

added stub for quotient paper; call with isabelle make qpaper

Cleaning of Int and FSet Examples

use the more general type-class at_base

deleted left-over code

simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base

use sort at_base instead of at

white spaces

avoided repeated dest of dt_info

tuned

factured out common functionality of prefixing the dt-names with a string

closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy

added some further problemetic tests

some tuning

moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base

merged

Rewrote FV code and included the function package.

merge

Function in Core Haskell

one more pass over the paper

more polishing on the paper

merged

some changes to the paper

rewrote eqvts_raw to be a symtab, that can be looked up

merge ???

infix for In

eliminated command so that all compiles

changed theorem_i to theorem....requires new Isabelle

tuned

tuned and cleaned

tuned and made to compile

added definition of raw-permutations to the new-parser

tuned

slight tuning

added a comment about a function where I am not sure who wrote it.

merged