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)

added a container for quotient constants (does not work yet though)

Lifting towards goal and manually finished the proof.

merge

Modifications while preparing the goal-directed version.

updated to new Theory_Data and to new Isabelle

Removed 'Toplevel.program' for polyml 5.3

Atomizing a "goal" theorems.

More code cleaning and commenting

Minor cleaning and removing of some 'handle _'.

Cleaning and commenting

Fixes for the other get_fun implementation.

permutation lifting works now also

merged

updated to new Isabelle version and added a new example file

Minor changes

merge

fold_rsp

tuned the code in quotient and quotient_def

More functionality for lifting list.cases and list.recs.

merged

removed typing information from get_fun in quotient_def; *potentially* dangerous

Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.

removed Simplifier.context

replaced check_term o parse_term by read_term

merged

Infrastructure for polymorphic types

Two new tests for get_fun. Second one fails.

Type instantiation in regularize

Description of regularize

Experiments with lifting partially applied constants.

more tuning

slightly tuned

merged

separated the quotient_def into a separate file

Experiments in Int

fixed definition of PLUS

simplified the quotient_def code

Lifting 'fold1.simps(2)' and some cleaning.

Playing with alpha_refl.

Alpha.induct now lifts automatically.

merge

applic_prs

simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated

Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP

merge

Preparing infrastructure for general FORALL_PRS

split quotient.ML into two files

slightly saner way of parsing the quotient_def

merged

changed Type.typ_match to Sign.typ_match

Fixes after optimization and preparing for a general FORALL_PRS

Optimization

Map does not fully work yet.

Fixed quotdata_lookup.

fixed problem with maps_update

merged

fixed the problem with types in map

Automatic computation of application preservation and manually finished "alpha.induct". Slow...