2010-02-26 |
Cezary Kaliszyk |
Change in signature of prove_const_rsp for general lifting.
|
changeset |
files
|
2010-02-26 |
Cezary Kaliszyk |
Permutation and FV_Alpha interface change.
|
changeset |
files
|
2010-02-26 |
Cezary Kaliszyk |
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Preparing the generalized lifting procedure
|
changeset |
files
|
2010-02-25 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-25 |
Christian Urban |
added ott-example about Leroy96
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Forgot to add one file.
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Split Terms into separate files and add them to tests.
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Move the eqvt code out of Terms and fixed induction for single-rule examples.
|
changeset |
files
|
2010-02-25 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-25 |
Christian Urban |
a few simplifications
|
changeset |
files
|
2010-02-25 |
Christian Urban |
first attempt to make sense out of the core-haskell definition
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Code for proving eqvt, still in Terms.
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Use eqvt infrastructure.
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Simple function eqvt code.
|
changeset |
files
|
2010-02-25 |
Christian Urban |
added IsaMakefile...but so far included only a test for the parser
|
changeset |
files
|
2010-02-25 |
Christian Urban |
moved Quot package to Attic (still compiles there with "isabelle make")
|
changeset |
files
|
2010-02-25 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-25 |
Christian Urban |
moved Nominal to "toplevel"
|
changeset |
files
|
2010-02-25 |
Cezary Kaliszyk |
Export perm_frees.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Restructuring the code in Perm
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Simplified and finised eqvt proofs for t1 and t5
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Define lifted perms.
|
changeset |
files
|
2010-02-24 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-24 |
Christian Urban |
parsing and definition of raw datatype and bv-function work (not very beautiful)
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
With permute_rsp we can lift the instance proofs :).
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Note the instance proofs, since they can be easily lifted.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
More refactoring and removed references to the global simpset in Perm.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Regularize finite support proof for trm1
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Made the fv-supp proof much more straightforward.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Regularize the proofs about finite support.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Respects of permute and constructors.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Generate fv_rsp automatically.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Define the constants automatically.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Rename also the lifted types to non-capital.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Use the infrastructure in LF. Much shorter :).
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
Final synchronization of names.
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
LF renaming part 3 (proper names of alpha equvalences)
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
LF renaming part 2 (proper fv functions)
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-24 |
Cezary Kaliszyk |
LF renaming part1.
|
changeset |
files
|
2010-02-24 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-24 |
Christian Urban |
parsing of function definitions almost works now; still an error with undefined constants
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
rsp for bv; the only issue is that it requires an appropriate induction principle.
|
changeset |
files
|
2010-02-23 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-23 |
Christian Urban |
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
rsp infrastructure.
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
Progress towards automatic rsp of constants and fv.
|
changeset |
files
|
2010-02-23 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-23 |
Christian Urban |
"raw"-ified the term-constructors and types given in the specification
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
Looking at proving the rsp rules automatically.
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
Minor beutification.
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
Define the quotient from ML
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
All works in LF but will require renaming.
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
Reordering in LF.
|
changeset |
files
|
2010-02-23 |
Cezary Kaliszyk |
Fixes for auxiliary datatypes.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Fixed pseudo_injectivity for trm4
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Testing auto equivp code.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
A tactic for final equivp
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
More equivp infrastructure.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
tactify transp
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
export the reflp and symp tacs.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Generalize atom_trans and atom_sym.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Some progress about transp
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
alpha-symmetric addons.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
alpha reflexivity
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Renaming.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Added missing description.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Added Brian's suggestion.
|
changeset |
files
|
2010-02-22 |
Cezary Kaliszyk |
Update TODO
|
changeset |
files
|
2010-02-21 |
Cezary Kaliszyk |
Removed bindings 'in itself' where possible.
|
changeset |
files
|
2010-02-20 |
Cezary Kaliszyk |
Some adaptation
|
changeset |
files
|
2010-02-19 |
Cezary Kaliszyk |
proof cleaning and standardizing.
|
changeset |
files
|
2010-02-19 |
Cezary Kaliszyk |
Automatic production and proving of pseudo-injectivity.
|
changeset |
files
|
2010-02-19 |
Cezary Kaliszyk |
Experiments for the pseudo-injectivity tactic.
|
changeset |
files
|
2010-02-19 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-19 |
Cezary Kaliszyk |
Constructing alpha_inj goal.
|
changeset |
files
|
2010-02-18 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-18 |
Christian Urban |
start work with the parser
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
First (non-working) version of alpha-equivalence
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Description of the fv procedure.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Testing auto constant lifting.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Fix for new Isabelle (primrec)
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Automatic lifting of constants.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Changed back to original version of trm5
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
The alternate version of trm5 with additional binding. All proofs work the same.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Code for handling atom sets.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Replace Terms by Terms2.
|
changeset |
files
|
2010-02-18 |
Cezary Kaliszyk |
Fixed proofs in Terms2 and found a mistake in Terms.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Terms2 with bindings for binders synchronized with bindings they are used in.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Cleaning of proofs in Terms.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Testing Fv
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Fix the strong induction principle.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Reorder
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Add bindings of recursive types by free_variables.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Bindings adapted to multiple defined datatypes.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Reorganization
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Now should work.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Some optimizations and fixes.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Simplified format of bindings.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Tested the Perm code; works everywhere in Terms.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Wrapped the permutation code.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Description of intended bindings.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Code for generating the fv function, no bindings yet.
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
indent
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-17 |
Cezary Kaliszyk |
Simplifying perm_eq
|
changeset |
files
|
2010-02-16 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-16 |
Cezary Kaliszyk |
indenting
|
changeset |
files
|
2010-02-16 |
Cezary Kaliszyk |
Minor
|
changeset |
files
|
2010-02-16 |
Cezary Kaliszyk |
Merge
|
changeset |
files
|
2010-02-16 |
Cezary Kaliszyk |
Ported Stefan's permutation code, still needs some localizing.
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Removed varifyT.
|
changeset |
files
|
2010-02-15 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-15 |
Christian Urban |
2-spaces rule (where it makes sense)
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Fixed the definition of less and finished the missing proof.
|
changeset |
files
|
2010-02-15 |
Christian Urban |
further tuning
|
changeset |
files
|
2010-02-15 |
Christian Urban |
small tuning
|
changeset |
files
|
2010-02-15 |
Christian Urban |
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
der_bname -> derived_bname
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Names of files.
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Finished introducing the binding.
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Synchronize the commands.
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Passing the binding to quotient_def
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Added a binding to the parser.
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
Second inline
|
changeset |
files
|
2010-02-15 |
Cezary Kaliszyk |
remove one-line wrapper.
|
changeset |
files
|
2010-02-12 |
Cezary Kaliszyk |
Undid the read_terms change; now compiles.
|
changeset |
files
|
2010-02-12 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-12 |
Cezary Kaliszyk |
renamed 'as' to 'is' everywhere.
|
changeset |
files
|
2010-02-12 |
Cezary Kaliszyk |
"is" defined as the keyword
|
changeset |
files
|
2010-02-12 |
Christian Urban |
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
|
changeset |
files
|
2010-02-12 |
Cezary Kaliszyk |
The lattice instantiations are gone from Isabelle/Main, so
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
the lam/bla example.
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Finished a working foo/bar.
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
fv_foo is not regular.
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Testing foo/bar
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Even when bv = fv it still doesn't lift.
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Added the missing syntax file
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Notation available locally
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Main renaming + fixes for new Isabelle in IntEx2.
|
changeset |
files
|
2010-02-11 |
Cezary Kaliszyk |
Merging QuotBase into QuotMain.
|
changeset |
files
|
2010-02-10 |
Christian Urban |
removed dead code
|
changeset |
files
|
2010-02-10 |
Christian Urban |
cleaned a bit
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
lowercase locale
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
hg-added the added file.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Changes from Makarius's code review + some noticed fixes.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
example with a respectful bn function defined over the type itself
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Finishe the renaming.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Another mistake found with OTT.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Fixed rbv6, when translating to OTT.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Some cleaning of proofs.
|
changeset |
files
|
2010-02-10 |
Christian Urban |
merged again
|
changeset |
files
|
2010-02-10 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
more minor space and bracket modifications.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
More changes according to the standards.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
A concrete example, with a proof that rbv is not regular and
|
changeset |
files
|
2010-02-09 |
Christian Urban |
proper declaration of types and terms during parsing (removes the varifyT when storing data)
|
changeset |
files
|
2010-02-09 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-09 |
Christian Urban |
slight correction
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
More about trm6
|
changeset |
files
|
2010-02-09 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
the specifications of the respects.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
trm6 with the 'Foo' constructor.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
removing unnecessary brackets
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
More indentation cleaning.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
'exc' -> 'exn' and more name and space cleaning.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Fully qualified exception names.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
More indentation, names and todo cleaning in the quotient package
|
changeset |
files
|
2010-02-09 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-09 |
Christian Urban |
a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
|
changeset |
files
|
2010-02-09 |
Christian Urban |
minor tuning
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Explicitly marked what is bound.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Cleaning and updating in Terms.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Looking at the trm2 example
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Fixed pattern matching, now the test in Abs works correctly.
|
changeset |
files
|
2010-02-08 |
Christian Urban |
added a test case
|
changeset |
files
|
2010-02-08 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-08 |
Christian Urban |
moved some lemmas to Nominal; updated all files
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
Comments.
|
changeset |
files
|
2010-02-08 |
Christian Urban |
slightly tuned
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
Proper context fixes lifting inside instantiations.
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
Fixed the context import/export and simplified LFex.
|
changeset |
files
|
2010-02-08 |
Christian Urban |
added 2 papers about core haskell
|
changeset |
files
|
2010-02-07 |
Christian Urban |
fixed lemma name
|
changeset |
files
|
2010-02-07 |
Christian Urban |
updated to latest Nominal2
|
changeset |
files
|
2010-02-06 |
Christian Urban |
minor
|
changeset |
files
|
2010-02-06 |
Christian Urban |
some tuning
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
Fixes for Bex1 removal.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
A procedure that properly instantiates the types too.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
More code abstracted away
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
A bit more intelligent and cleaner code.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
A proper version of the attribute
|
changeset |
files
|
2010-02-05 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-05 |
Christian Urban |
eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
|
changeset |
files
|
2010-02-04 |
Cezary Kaliszyk |
The automatic lifting translation function, still with dummy types,
|
changeset |
files
|
2010-02-04 |
Cezary Kaliszyk |
Quotdata_dest needed for lifting theorem translation.
|
changeset |
files
|
2010-02-04 |
Christian Urban |
fixed (permute_eqvt in eqvts makes this simpset always looping)
|
changeset |
files
|
2010-02-04 |
Christian Urban |
rollback of the test
|
changeset |
files
|
2010-02-04 |
Christian Urban |
linked versions - instead of copies
|
changeset |
files
|
2010-02-04 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-04 |
Christian Urban |
restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
More let-rec experiments
|
changeset |
files
|
2010-02-03 |
Christian Urban |
proposal for an alpha equivalence
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Lets different.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Simplified the proof.
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
proved that bv for lists respects alpha for terms
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Finished remains on the let proof.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Lets are ok.
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
added type-scheme example
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Definitions for trm5
|
changeset |
files
|
2010-02-03 |
Christian Urban |
another adaptation for the eqvt-change
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
fixed proofs that broke because of eqvt
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Minor fix.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
alpha5 pseudo-injective
|
changeset |
files
|
2010-02-03 |
Christian Urban |
fixed proofs in Abs.thy
|
changeset |
files
|