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