fixed examples in IntEx and FSet

merged

fixed previous commit

Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.

Merged comment

Integrated Stefan's tactic and changed substs to simps with empty context.

some slight tuning of the apply-tactic

annotated a proof with all steps and simplified LAMBDA_RES_TAC

Merge

The magical code from Stefan, will need to be integrated in the Simproc.

replaced FIRST' (map rtac list) with resolve_tac list

Simplifying arguments; got rid of trans2_thm.

Cleaning of LFex. Lambda_prs fails to unify in 2 places.

Recommit

Removing arguments of tactics: absrep, rel_refl, reps_same are computed.

More cleaning in QuotMain, identity handling.

Minor cleaning

tuned

some tuning

simplified gen_frees_tac and properly named abstracted variables

removed CHANGED'

introduced a separate lemma for id_simps

renamed inj_REPABS to inj_repabs_trm

tuned comments and moved slightly some code

deleted obsolete qenv code

renamed REGULARIZE to be regularize

more tuning

deleted get_fun_old and stuff

recommited changes of comments

Merge Again

Merged

tuned comments

some diagnostic code for r_mk_comb

introduced a new property for Ball and ===> on the left

fixed QuotList

changed left-res

Manually regularized akind_aty_atrm.induct

Playing with Monos in LFex.

Fixed FSet after merge.

merged

test with monos

applic_prs

polishing

reordered the code

Moved exception handling to QuotMain and cleaned FSet.

Merge

Finished manual lifting of list_induct_part :)

comments tuning and slight reordering

Merge

More moving from QuotMain to UnusedQuotMain

deleted some obsolete diagnostic code

Removed unused things from QuotMain.

All examples work again.

cleaning in MyInt

lambda_prs and cleaning the existing examples.

merged

fixed the problem with generalising variables; at the moment it is quite a hack

Ho-matching failures...

changed unification to matching

unification

Lambda & SOLVED' for new quotient_tac

merged

Conversion

The non-working procedure_tac.

merged

use error instead of raising our own exception

Fixes to the tactic after quotient_tac changed.

merged

added a prepare_tac

TRY' for clean_tac

Moved cleaning to QuotMain

New cleaning tactic

explicit phases for the cleaning

Separate regularize_tac

Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.

More fixes for inj_REPABS

addded a tactic, which sets up the three goals of the `algorithm'

fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)

merged

tuned some comments

Another not-typechecking regularized term.

domain_type in regularizing equality

More theorems lifted in the goal-directed way.

Finished temporary goal-directed lift_theorem wrapper.

merged

a version of inj_REPABS (needs to be looked at again later)

Fixes for atomize

merge

lift_thm with a goal.

slight change in code layout

Fixes for new code

Removing dead code

Move atomize_goal to QuotMain

Removed second implementation of Regularize/Inject from FSet.

Moved new repabs_inj code to QuotMain

New repabs behaves the same way as old one.

code review with Cezary

The other branch does not seem to work...

Fixes for recent changes.

updated to Isabelle 22nd November

a little tuning of comments

slight tuning

some debugging code, but cannot find the place where the cprems_of exception is raised

tried to prove the repabs_inj lemma, but failed for the moment

my first version of repabs injection

tuned

tunded

tuned

flagged qenv-stuff as obsolete

simplified get_fun so that it uses directly rty and qty, instead of qenv

started regularize of rtrm/qtrm version; looks quite promising

updated to new Isabelle

fixed the storage of qconst definitions

Still don't know how to do the proof automatically.

added some tracing information to all phases of lifting to the function lift_thm

merge of the merge?

merged

added a FIXME commment

looking up data in quot_info works now (needs qualified string)

changed the quotdata to be a symtab table (needs fixing)