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.

Used symmetric definitions. Moved quotient_rsp to QuotMain.

Proved foldl_rsp and ho_map_rsp

moved all_prs and ex_prs out from the conversion into the simplifier

further cleaning

Merge

Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.

simplified inj_repabs_trm

merged

merged

merged

simpler version of clean_tac

Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.

Solutions to IntEx tests.

made some slight simplifications to the examples

added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet

tuned code

merged

not yet quite functional treatment of constants

Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)

Changing FOCUS to CSUBGOAL (part 1)

abs_rep as ==

Cleaning the Quotients file

Minor renames and moving

Cleaning/review of QuotScript.

More cleaning

more name cleaning and removing

More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList

Cleaning & Renaming coming from QuotList

Cleaning in Quotients

Even more name changes and cleaning

More code cleaning and name changes

merge

merged

smaller theory footprint

merged

merge

smaller theory footprint

More name changes

Naming changes

code cleaning and renaming

merge

Removed previous inj_repabs_tac

some tuning

merge

rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.

merged

merged

Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.

compose_tac instead of rtac to avoid unification; some code cleaning.

Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.

Using APPLY_RSP1; again a little bit faster.

Fixes after big merge.

The big merge; probably non-functional.

Testing the new tactic everywhere

First version of the deterministic rep-abs-inj-tac.

Changing = to \<equiv> in case if we want to use simp.

Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac

merge

Made your version work again with LIST_REL_EQ.

the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied

removed quot argument...not all examples work anymore

merged

merged

first version of internalised quotient theorems; added FIXME-TODO

further dead code

Reintroduced varifyT; we still need it for permutation definition.

Updated the examples

Fixed previous mistake

defs used automatically by clean_tac

Added qoutient_consts dest for getting all the constant definitions in the cleaning step.

Added the definition to quotient constant data.

removing unused code

merged

deleted some dead code

Included all_prs and ex_prs in the lambda_prs conversion.

further simplification

simplified lambda_prs_conv

deleted now obsolete argument rty everywhere

deleted tests at the beginning of QuotMain

Experiments with OPTION_map

merge

More experiments with higher order quotients and theorems with non-lifted constants.

merged

Lifting to 2 different types :)

New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.