Quot/quotient_def.ML
2010-02-18 Cezary Kaliszyk Automatic lifting of constants.
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 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 remove one-line wrapper.
2010-02-12 Cezary Kaliszyk Undid the read_terms change; now compiles.
2010-02-12 Cezary Kaliszyk "is" defined as the keyword
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2.
2010-02-10 Christian Urban merged
2010-02-09 Cezary Kaliszyk More indentation, names and todo cleaning in the quotient package
2010-01-27 Christian Urban use of equiv_relation_chk in quotient_term
2010-01-14 Christian Urban tuned quotient_def.ML and cleaned somewhat LamEx.thy
2010-01-14 Cezary Kaliszyk Finished organising an efficient datastructure for qconst_info.
2010-01-14 Cezary Kaliszyk Undid changes from symtab to termtab, since we need to lookup specialized types.
2010-01-13 Cezary Kaliszyk Better error message for definition failure.
2010-01-13 Cezary Kaliszyk Stored Termtab for constant information.
2010-01-13 Christian Urban tuned
2010-01-13 Christian Urban merged
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 Cezary Kaliszyk minor comment editing
2010-01-10 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples.
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban fixed comment errors
2010-01-01 Christian Urban some slight tuning
2009-12-31 Christian Urban renamed transfer to transform (Markus)
less more (0) -30 tip