nominal2: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip

Bindings adapted to multiple defined datatypes.
2010-02-17, by Cezary Kaliszyk
Reorganization
2010-02-17, by Cezary Kaliszyk
Now should work.
2010-02-17, by Cezary Kaliszyk
Some optimizations and fixes.
2010-02-17, by Cezary Kaliszyk
Simplified format of bindings.
2010-02-17, by Cezary Kaliszyk
Tested the Perm code; works everywhere in Terms.
2010-02-17, by Cezary Kaliszyk
Wrapped the permutation code.
2010-02-17, by Cezary Kaliszyk
Description of intended bindings.
2010-02-17, by Cezary Kaliszyk
Code for generating the fv function, no bindings yet.
2010-02-17, by Cezary Kaliszyk
merge
2010-02-17, by Cezary Kaliszyk
indent
2010-02-17, by Cezary Kaliszyk
merge
2010-02-17, by Cezary Kaliszyk
Simplifying perm_eq
2010-02-17, by Cezary Kaliszyk
merge
2010-02-16, by Cezary Kaliszyk
indenting
2010-02-16, by Cezary Kaliszyk
Minor
2010-02-16, by Cezary Kaliszyk
Merge
2010-02-16, by Cezary Kaliszyk
Ported Stefan's permutation code, still needs some localizing.
2010-02-16, by Cezary Kaliszyk
merge
2010-02-15, by Cezary Kaliszyk
Removed varifyT.
2010-02-15, by Cezary Kaliszyk
merged
2010-02-15, by Christian Urban
2-spaces rule (where it makes sense)
2010-02-15, by Christian Urban
merge
2010-02-15, by Cezary Kaliszyk
Fixed the definition of less and finished the missing proof.
2010-02-15, by Cezary Kaliszyk
further tuning
2010-02-15, by Christian Urban
small tuning
2010-02-15, by Christian Urban
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
2010-02-15, by Christian Urban
der_bname -> derived_bname
2010-02-15, by Cezary Kaliszyk
Names of files.
2010-02-15, by Cezary Kaliszyk
Finished introducing the binding.
2010-02-15, by Cezary Kaliszyk
Synchronize the commands.
2010-02-15, by Cezary Kaliszyk
Passing the binding to quotient_def
2010-02-15, by Cezary Kaliszyk
Added a binding to the parser.
2010-02-15, by Cezary Kaliszyk
Second inline
2010-02-15, by Cezary Kaliszyk
remove one-line wrapper.
2010-02-15, by Cezary Kaliszyk
Undid the read_terms change; now compiles.
2010-02-12, by Cezary Kaliszyk
merge
2010-02-12, by Cezary Kaliszyk
renamed 'as' to 'is' everywhere.
2010-02-12, by Cezary Kaliszyk
"is" defined as the keyword
2010-02-12, by Cezary Kaliszyk
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
2010-02-12, by Christian Urban
The lattice instantiations are gone from Isabelle/Main, so
2010-02-12, by Cezary Kaliszyk
the lam/bla example.
2010-02-11, by Cezary Kaliszyk
Finished a working foo/bar.
2010-02-11, by Cezary Kaliszyk
fv_foo is not regular.
2010-02-11, by Cezary Kaliszyk
Testing foo/bar
2010-02-11, by Cezary Kaliszyk
Even when bv = fv it still doesn't lift.
2010-02-11, by Cezary Kaliszyk
Added the missing syntax file
2010-02-11, by Cezary Kaliszyk
Notation available locally
2010-02-11, by Cezary Kaliszyk
Main renaming + fixes for new Isabelle in IntEx2.
2010-02-11, by Cezary Kaliszyk
Merging QuotBase into QuotMain.
2010-02-11, by Cezary Kaliszyk
removed dead code
2010-02-10, by Christian Urban
cleaned a bit
2010-02-10, by Christian Urban
lowercase locale
2010-02-10, by Cezary Kaliszyk
hg-added the added file.
2010-02-10, by Cezary Kaliszyk
Changes from Makarius's code review + some noticed fixes.
2010-02-10, by Cezary Kaliszyk
example with a respectful bn function defined over the type itself
2010-02-10, by Cezary Kaliszyk
Finishe the renaming.
2010-02-10, by Cezary Kaliszyk
Another mistake found with OTT.
2010-02-10, by Cezary Kaliszyk
merge
2010-02-10, by Cezary Kaliszyk
Fixed rbv6, when translating to OTT.
2010-02-10, by Cezary Kaliszyk