modified for new binding format - hope it is the intended one

further code-refactoring in the parser

The new alpha-equivalence and testing in Trm2 and Trm5.

slight simplification of the raw-decl generation

Example that shows that current alpha is wrong.

added example from my phd

streamlined parser

generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"

More about the general lifting procedure.

Update TODO

Progress with general lifting procedure.

RSP of perms can be shown in one go.

Change in signature of prove_const_rsp for general lifting.

Permutation and FV_Alpha interface change.

To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.

merge

Preparing the generalized lifting procedure

merged

added ott-example about Leroy96

Forgot to add one file.

Split Terms into separate files and add them to tests.

merge

Move the eqvt code out of Terms and fixed induction for single-rule examples.

merged

a few simplifications

first attempt to make sense out of the core-haskell definition

Code for proving eqvt, still in Terms.

Use eqvt infrastructure.

Simple function eqvt code.

added IsaMakefile...but so far included only a test for the parser

moved Quot package to Attic (still compiles there with "isabelle make")

merged

moved Nominal to "toplevel"

Export perm_frees.

Restructuring the code in Perm

Simplified and finised eqvt proofs for t1 and t5

merge

Define lifted perms.

merged

parsing and definition of raw datatype and bv-function work (not very beautiful)

With permute_rsp we can lift the instance proofs :).

Note the instance proofs, since they can be easily lifted.

More refactoring and removed references to the global simpset in Perm.

Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.

Regularize finite support proof for trm1

Made the fv-supp proof much more straightforward.

Regularize the proofs about finite support.

Respects of permute and constructors.

Generate fv_rsp automatically.

Define the constants automatically.

Rename also the lifted types to non-capital.

Use the infrastructure in LF. Much shorter :).

Final synchronization of names.

LF renaming part 3 (proper names of alpha equvalences)

LF renaming part 2 (proper fv functions)

merge

LF renaming part1.

merged

parsing of function definitions almost works now; still an error with undefined constants

merge

rsp for bv; the only issue is that it requires an appropriate induction principle.

merged

declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types

rsp infrastructure.

merge

Progress towards automatic rsp of constants and fv.

merged

"raw"-ified the term-constructors and types given in the specification

Looking at proving the rsp rules automatically.

Minor beutification.

Define the quotient from ML

All works in LF but will require renaming.

Reordering in LF.

Fixes for auxiliary datatypes.

Fixed pseudo_injectivity for trm4

Testing auto equivp code.

A tactic for final equivp

More equivp infrastructure.

tactify transp

export the reflp and symp tacs.

Generalize atom_trans and atom_sym.

Some progress about transp

alpha-symmetric addons.

alpha reflexivity

Renaming.

Added missing description.

Added Brian's suggestion.

Update TODO

Removed bindings 'in itself' where possible.

Some adaptation

proof cleaning and standardizing.

Automatic production and proving of pseudo-injectivity.

Experiments for the pseudo-injectivity tactic.

merge

Constructing alpha_inj goal.

merged

start work with the parser

Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.

First (non-working) version of alpha-equivalence

Description of the fv procedure.

Testing auto constant lifting.

Fix for new Isabelle (primrec)

Automatic lifting of constants.

Changed back to original version of trm5

The alternate version of trm5 with additional binding. All proofs work the same.

Code for handling atom sets.

Replace Terms by Terms2.

Fixed proofs in Terms2 and found a mistake in Terms.

Terms2 with bindings for binders synchronized with bindings they are used in.

Cleaning of proofs in Terms.

Testing Fv

Fix the strong induction principle.

Reorder

Add bindings of recursive types by free_variables.

Bindings adapted to multiple defined datatypes.

Reorganization

Now should work.

Some optimizations and fixes.

Simplified format of bindings.

Tested the Perm code; works everywhere in Terms.

Wrapped the permutation code.

Description of intended bindings.

Code for generating the fv function, no bindings yet.

merge

indent

merge

Simplifying perm_eq

merge

indenting

Minor

Merge

Ported Stefan's permutation code, still needs some localizing.

merge

Removed varifyT.

merged

2-spaces rule (where it makes sense)

merge

Fixed the definition of less and finished the missing proof.

further tuning

small tuning

tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy

der_bname -> derived_bname

Names of files.

Finished introducing the binding.

Synchronize the commands.

Passing the binding to quotient_def

Added a binding to the parser.

Second inline

remove one-line wrapper.

Undid the read_terms change; now compiles.

merge

renamed 'as' to 'is' everywhere.

"is" defined as the keyword

moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned

The lattice instantiations are gone from Isabelle/Main, so this can be removed.

the lam/bla example.

Finished a working foo/bar.

fv_foo is not regular.

Testing foo/bar

Even when bv = fv it still doesn't lift.

Added the missing syntax file

Notation available locally

Main renaming + fixes for new Isabelle in IntEx2.

Merging QuotBase into QuotMain.

removed dead code

cleaned a bit

lowercase locale

hg-added the added file.

Changes from Makarius's code review + some noticed fixes.

example with a respectful bn function defined over the type itself

Finishe the renaming.

Another mistake found with OTT.

merge

Fixed rbv6, when translating to OTT.

Some cleaning of proofs.

merged again

merged

more minor space and bracket modifications.

More changes according to the standards.

A concrete example, with a proof that rbv is not regular and with proofs of induction and pseudo-injectivity that require this

proper declaration of types and terms during parsing (removes the varifyT when storing data)

merged

slight correction

merge

More about trm6

merged

the specifications of the respects.

trm6 with the 'Foo' constructor.

removing unnecessary brackets

More indentation cleaning.

'exc' -> 'exn' and more name and space cleaning.

Fully qualified exception names.

merge

More indentation, names and todo cleaning in the quotient package

merged

a few more attempts to show the equivalence between old and new way of defining alpha-equivalence

minor tuning

Explicitly marked what is bound.

Cleaning and updating in Terms.

Looking at the trm2 example

Fixed pattern matching, now the test in Abs works correctly.

added a test case

merged

moved some lemmas to Nominal; updated all files

merge

Comments.

slightly tuned

Proper context fixes lifting inside instantiations.

Fixed the context import/export and simplified LFex.

added 2 papers about core haskell

fixed lemma name

updated to latest Nominal2

minor

some tuning

merge

merge

Fixes for Bex1 removal.

Cleaned Terms using [lifted] and found a workaround for the instantiation problem.

A procedure that properly instantiates the types too.

More code abstracted away

A bit more intelligent and cleaner code.

merge

A proper version of the attribute

merged

eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts

The automatic lifting translation function, still with dummy types, but works everywhere in the LF example.

Quotdata_dest needed for lifting theorem translation.

fixed (permute_eqvt in eqvts makes this simpset always looping)

rollback of the test

linked versions - instead of copies

merged

restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw

More let-rec experiments

proposal for an alpha equivalence

Lets different.

Simplified the proof.

merged

proved that bv for lists respects alpha for terms

Finished remains on the let proof.

merge

Lets are ok.

merged

added type-scheme example

merge

Definitions for trm5

another adaptation for the eqvt-change

merged

fixed proofs that broke because of eqvt

Minor fix.

merge

alpha5 pseudo-injective

fixed proofs in Abs.thy

merged

added a first eqvt_tac which pushes permutations inside terms

The alpha-equivalence relation for let-rec. Not sure if correct...

Starting with a let-rec example.

Minor

Some cleaning and eqvt proof

The trm1_support lemma explicitly and stated a strong induction principle.

More ingredients in Terms.

Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)

More in Terms

First experiments in Terms.

LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.

Disambiguating the syntax.

Minor uncommited changes from LamEx2.

Some equivariance machinery that comes useful in LF.

Generalized the eqvt proof for single binders.

With induct instead of induct_tac, just one induction is sufficient.

General alpha_gen_trans for one-variable abstraction.

With unfolding Rep/Abs_eqvt no longer needed.

Lam2 finished apart from Rep_eqvt.

merge

All should be ok now.

repaired according to changes in Abs.thy

added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case

cleaned

updated from huffman

updated from nominal-huffman

Fixed wrong rename.

merge

Lambda based on alpha_gen, under construction.

updated from huffman - repo

renamed Abst/abst to Abs/abs

got rid of RAbst type - is now just pairs

Monotonicity of ~~gen, needed for using it in inductive definitions.

The current state of fv vs supp proofs in LF.

merge

More proofs in the LF example.

merged

slight tuning

renamed function according to the name of the constant

fixed problem with Bex1_rel renaming

Ported LF to the generic lambda and solved the simpler _supp cases.

merged

introduced a generic alpha (but not sure whether it is helpful)

More in the LF example in the new nominal way, all is clear until support.

Fixed the induction problem + some more proofs.

equivariance of rfv and alpha.

Added the experiments with fun and function.

now also final step is proved - the supp of lambdas is now completely characterised

the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms

improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions

merged

general abstraction operator and complete characterisation of its support and freshness

Ported existing part of LF to new permutations and alphas.

attempt of a general abstraction operator

attempt to prove equivalence between alpha definitions

End of renaming.

Minor when looking at lam.distinct and lam.inject

Renamed Bexeq to Bex1_rel

Substracting bounds from free variables.

Improper interface for datatype and function packages and proper interface lateron.

merged

minor

test about supp/freshness for lam (old proofs work in principle - for single binders)

Recommited the changes for nitpick

Correct types which fixes the printing.

fv for subterms

Fix the problem with later examples. Maybe need to go back to textual specifications.

Some processing of variables in constructors to get free variables.

Parsing of the input as terms and types, and passing them as such to the function package.

Undid the parsing, as it is not possible with thy->lthy interaction.

merge

Some cleaning of thy vs lthy vs context.

merged

tuned comment

completely ported

Another string in the specification.

Variable takes a 'name'.

merge

When commenting discovered a missing case of Babs->Abs regularization.

merged

mostly ported Terms.thy to new Nominal

merge

Commenting regularize

very rough example file for how nominal2 specification can be parsed

reordered cases in regularize (will be merged into two cases)

use of equiv_relation_chk in quotient_term

some slight tuning

added Terms to Nominal - Instantiation of two types does not work (ask Florian)

added another example with indirect recursion over lists

just moved obsolete material into Attic

added an LamEx example together with the new nominal infrastructure

Bex1_Bexeq_regular.

Hom Theorem with exists unique

2 cases for regularize with split, lemmas with split now lift.

Simpler statement that has the problem.

Found a term that does not regularize.

A triple is still ok.

Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.

Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.

Sigma cleaning works with split_prs (still manual proof).

tuned

merged

cleaning of QuotProd; a little cleaning of QuotList

added prs and rsp lemmas for Inl and Inr

used split_option_all lemma

used the internal Option.map instead of custom option_map

Generalized split_prs and split_rsp

All eq_reflections apart from the one of 'id_apply' can be removed.

continued

More eqreflection/equiv cleaning.

more eq_reflection & other cleaning.

Removing more eq_reflections.

ids *cannot* be object equalities

re-inserted lemma in QuotList

added prs and rsp lemmas for Some and None

tuned proofs (mainly in QuotProd)

properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list

renamed QuotScript to QuotBase

cleaned some theorems

test with splits

The alpha equivalence relations for structures in 'Terms'

More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.

Trying to define hom for the lifted type directly.

Proper alpha equivalence for Sigma calculus.

Changed fun_map and rel_map to definitions.

Lifted Peter's Sigma lemma with Ex1.

Automatic injection of Bexeq

Automatic cleaning of Bexeq<->Ex1 theorems.

Using Bexeq_rsp, and manually lifted lemma with Ex1.

Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.

The missing rule.

Ex1 -> Bex1 Regularization, Preparing Exeq.

Added the Sigma Calculus example

Better error messages for non matching quantifiers.

Statement of term1_hom_rsp

proved that the function is a function

term1_hom as a function

A version of hom with quantifiers.

added permutation functions for the raw calculi

fixed broken (partial) proof

used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on

liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals

added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions

tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely

merged

added free_variable function (do not know about the algorithm yet)

hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.

slight tuning of relation_error

Appropriate respects and a statement of the lifted hom lemma

recursion-hom for lambda

Incorrect version of the homomorphism lemma

trivial

tuned quotient_typ.ML

tuned quotient_def.ML and cleaned somewhat LamEx.thy

a few more lemmas...except supp of lambda-abstractions

removed one sorry

nearly all of the proof

right generalisation

First subgoal.

setup for strong induction

exported absrep_const for nitpick.

minor

Simplified matches_typ.

added bound-variable functions to terms

merged

added 3 calculi with interesting binding structure

produce defs with lthy, like prs and ids

Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.

Finished organising an efficient datastructure for qconst_info.

Undid changes from symtab to termtab, since we need to lookup specialized types.

Moved the matches_typ function outside a?d simplified it.

one more item in the list of Markus

Put relation_error as a separate function.

Better error message for definition failure.

merge

Stored Termtab for constant information.

merged

deleted SOLVED'

Removed the 'oops' in IntEx.

tuned

added SOLVED' which is now part of Isabelle....must be removed eventually

merged

tuned

absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"

More indenting, bracket removing and comment restructuring.

Finished replacing OO by OOO

Change OO to OOO in FSet3.

minor comment editing

modifying comments/indentation in quotient_term.ml

Cleaning comments, indentation etc in quotient_tacs.

No more exception handling in rep_abs_rsp_tac

handle all is no longer necessary in lambda_prs.

removed 3 hacks.

Updated some comments.

merge

Removed exception handling from equals_rsp_tac.

added an abbreviation for OOO

merge

Undid the non-working part.

started to adhere to Wenzel-Standard

Changing exceptions to 'try', part 1.

removed quotdata_lookup_type

Fix for testing matching constants in regularize.

tuned previous commit further

the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"

introduced separate match function

removed obsolete equiv_relation and rnamed new_equiv_relation

New_relations, all works again including concat examples.

map and rel simps for all quotients; needed when changing the relations to aggregate ones.

id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.

Experimients with fconcat_insert

Modifications for new_equiv_rel, part2

Modifictaions for new_relation.

Proved concat_empty.

Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.

some cleaning.

First generalization.

The working proof of the special case.

Reduced the proof to two simple but not obvious to prove facts.

More cleaning and commenting AbsRepTest. Now tests work; just slow.

cleaning in AbsRepTest.

Further in the proof

Tried to prove the lemma manually; only left with quotient proofs.

Sledgehammer bug.

merge

Trying the proof

merged

Struggling with composition

Trying to state composition quotient.

proper handling of error messages (code copy - maybe this can be avoided)

added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)

Readded 'regularize_to_injection' which I believe will be needed.

added a warning to the quotient_type definition, if a map function is missing

tuned

a slight change to abs/rep generation

tuned

fixed comment errors

some slight tuning

renamed transfer to transform (Markus)

some small changes

added a functor that allows checking what is added to the theorem lists

corrected wrong [quot_respect] attribute; tuned

renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy

added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)

as expected problems occure when lifting concat lemmas

tuned

commeted the absrep function

generalised absrep function; needs consolidation

tuned

added sanity checks for quotient_type

made the quotient_type definition more like typedef; now type variables need to be explicitly given

used Local_Theory.declaration for storing quotdata

tuning

renamed some fields in the info records

modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants

cleaed a bit function mk_typedef_main

renamed QUOT_TYPE to Quot_Type

explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions

corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file

added "Highest Priority" category; and tuned slightly code

added a print_maps command; updated the keyword file accordingly

renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions

tuned

moved get_fun into quotient_term; this simplifies the overall including structure of the package

tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works

on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst

simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed

used eq_reflection not with OF, but directly in @{thm ...}

cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)

get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO

on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file

renamed "quotient" command to "quotient_type"; needs new keyword file to be installed

this file is now obsolete; replaced by isar-keywords-quot.el

with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place

added a very old paper about Quotients in Isabelle (related work)

avoided global "open"s - replaced by local "open"s

small tuning

various tunings; map_lookup now raises an exception; addition to FIXME-TODO

minor cleaning

moved the QuotMain code into two ML-files

complete fix for IsaMakefile

first fix

merged

added a paper for possible notes

Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.

lambda_prs & solve_quotient_assum cleaned.

some commenting

Fixed previous commit.

merge

Moved DETERM inside Repeat & added SOLVE around quotient_tac.

merge.

FIXME/TODO.

reply to question in code

Reply in code.

Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.

a few code annotations

another pass on apply_rsp

managed to simplify apply_rsp

tried to simplify apply_rsp_tac; failed at the moment; added some questions

some trivial changes

trivial cleaning of make_inst

tried to improve test; but fails

merged

annotated some questions to the code; some simple changes

Answering the question in code.

merged

trivial

tuned code

Minor

Some proofs.

Proof of finite_set_storng_cases_raw.

A bracket was missing; with it proved the 'definitely false' lemma.

renamed quotient.ML to quotient_typ.ML

merged

tuned

started to have a look at it; redefined the relation

More name and indentation cleaning.

Merge + Added LarryInt & Fset3 to tests.

Renaming

merged

deleted struct_match by Pattern.match (fixes a problem in LarryInt)

FSet3 minor fixes + cases

added Int example from Larry

Added FSet3 with a formalisation of finite sets based on Michael's one.

Updated TODO list together.

Merge

More theorem renaming.

Renamed theorems in IntEx2 to conform to names in Int.

Updated comments.

merged

tuned

renamed Larrys example

New syntax for definitions.

changed error message

reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case

slightly tuned

merged

added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages

added maps-printout and tuned some comments

Option and Sum quotients.

Regularized the hard lemma.

Simplification of Babses for regularize; will probably become injection

Found the problem with ttt3.

minor

Moved Unused part of locale to Unused QuotMain.

Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.

Removed 'Presburger' as it introduces int & other minor cleaning in Int2.

more tuning

tuned

simplified the instantiation of QUOT_TRUE in procedure_tac

completed previous commit

deleted DT/NDT diagnostic code

moved the interpretation code into Unused.thy

added an attempt to get a finite set theory

removed memb and used standard mem (member from List.thy)

merged

simplified proofs

removed quot_respect attribute of a non-standard lemma

With int_of_nat as a quotient_def, lemmas about it can be easily lifted.

merged

naming in this file cannot be made to agree to the original (PROBLEM?)

Lifted some kind of induction.

more proofs in IntEx2

Finished one proof in IntEx2.

slightly more on IntEx2

proved (with a lot of pain) that times_raw is respectful

merged

fixed minor stupidity

Exception handling.

Code cleaning.

merge

foldr_rsp.

tuned

merge

Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.

deleted make_inst3

tuned

tuned

moved function and tuned comment

improved fun_map_conv

Arbitrary number of fun_map_tacs.

Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.

tuned code

tuned the examples and flagged the problematic cleaning lemmas in FSet

merged

implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges

merge

manually cleaned the hard lemma.

merged

decoupled QuotProd from QuotMain and also started new cleaning strategy

merge

An example which is hard to lift because of the interplay between lambda_prs and unfolding.

proper formulation of all preservation theorems

started to reformulate preserve lemmas

properly set up the prs_rules

merged

added preserve rules to the cleaning_tac

merge

cleaning.

merged

chnaged syntax to "lifting theorem"

changed names of attributes

merge

Manual regularization of a goal in FSet.

merged

added methods for the lifting_tac and the other tacs

make_inst3

Merge

trans2 replaced with equals_rsp_tac

corrected name of FSet in ROOT.ML

Made fset work again to test all.

Finished the proof of ttt2 and found bug in regularize when trying ttt3.

Another lambda example theorem proved. Seems it starts working properly.

Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned

Proper checked map_rsp.

Nitpick found a counterexample for one lemma.

Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.

It also regularizes.

inj_repabs also works.

merge

An example of working cleaning for lambda lifting. Still not sure why Babs helps.

tuned

the lift_tac produces a warning message if one of the three automatic proofs fails

added a thm list for ids

removed a fixme: map_info is now checked

tuning of the code

merged

removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>

3 lambda examples in FSet. In the last one regularize_term fails.

Handling of errors in lambda_prs_conv.

babs_prs

clarified the function examples

first attempt to deal with Babs in regularise and cleaning (not yet working)

isabelle make tests all examples

merge

make_inst for lambda_prs where the second quotient is not identity.

added "end" to each example theory

List moved after QuotMain

cleaning

final move

directory re-arrangement

inj_repabs_tac handles Babs now.

Fix of regularize for babs and proof of babs_rsp.

Using pair_prs; debugging the error in regularize of a lambda.

QuotProd with product_quotient and a 3 respects and preserves lemmas.

merge

3 new example thms in MyInt; reveal problems with handling of lambdas; regularize fails with "Loose Bound".

simplified the regularize simproc

now simpler regularize_tac with added solver works

removed usage of HOL_basic_ss by using a slighly extended version of empty_ss

merged

fixed examples

Fix IntEx2 for equiv_list

merged

working state again

added a theorem list for equivalence theorems

Merge

Name changes.

Solved all quotient goals.

updated Isabelle and deleted mono rules

more tuning of the code

puting code in separate sections

Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.

merge

Simpler definition code that works with any type maps.

working on lambda_prs with examples; polished code of clean_tac

renamed lambda_allex_prs

added more to IntEx2

merged

added new example for Ints; regularise does not work in all instances

Definitions folded first.