simplified the unlam_def function

added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)

used prop_of to get the term of a theorem (replaces crep_thm)

Merged

First theorem with quantifiers. Learned how to use sledgehammer.

simplified the storage of the map-functions by using TheoryDataFun

Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.

used new cong_tac

First version of handling of the universal quantifier

Handling abstraction correctly.

second test

Test line

Partially fix lifting of card_suc. The quantified variable still needs to be changed.

Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.

Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.

Merged

added name to prove

consistent state

some tuning of my code

Cleanup

Merged

Cleaning the code with Makarius

Instnatiation with a schematic variable

added ctxt as explicit argument to build_goal; tuned

slightly tuned the comment for unlam

fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x

tuned slightly one proof

A version of the tactic that exports variables correctly. It still does not know how to instantiate the obtained theorems.

Minor cleaning: whitespace, commas etc.

Correctly handling abstractions while building goals Use DatatypeAux cong_tac instead of own functions since it handles universal quantifiers properly.

Minor cleanup

Found the source for the exception and added a handle for it.

Make the tactic use Trueprop_cong and atomize.

Proper code for getting the prop out of the theorem.

Using "atomize" the versions with arbitrary Trueprops can be proven.

Proper definition of CARD and some properties of it. Translation should now support Pure assumptions and Trueprops anywhere, but a problem needs to be fixed with the tactic.

some comments

merged

slight tuning

The tactic with REPEAT, CHANGED and a proper simpset.

Merged with my changes from the morning: further working on the tactic and produced goals.

some more beautification

beautification of some proofs

Added more useful quotient facts.

Testing the tactic further.

The tactic still only for fset

Infrastructure for the tactic

More naming/binding suggestions from Makarius

Code cleanup

Cleaning the code

Generalized interpretation, works for all examples.

Fixes after suggestions from Makarius: - indentation - lowercase/uppercase - axioms -> axiomatization - proper operator priorities - proper exception handling

More examples.

Use metavariables in the 'non-lambda' definitions

Make both kinds of definitions.

Changed to the use of "modern interface" (removed the _cmd and passing of strings) Fixed Trueprop handling and the first proof starts working properly.

Initial version of the function that builds goals.

- Build an interpretation for fset from ML level and use it - Added CARD

added the prove command

Fixed

tuned

UNION - Append theorem

update

updated slightly

initial commit