Quot/Examples/LFex.thy
2009-12-22 Christian Urban simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
2009-12-19 Christian Urban on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
2009-12-19 Christian Urban renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
2009-12-12 Christian Urban trivial
2009-12-11 Cezary Kaliszyk New syntax for definitions.
2009-12-10 Christian Urban moved the interpretation code into Unused.thy
2009-12-09 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-08 Christian Urban tuned the examples and flagged the problematic cleaning lemmas in FSet
2009-12-08 Christian Urban changed names of attributes
2009-12-07 Christian Urban removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
2009-12-07 Christian Urban isabelle make tests all examples
2009-12-07 Cezary Kaliszyk List moved after QuotMain
2009-12-07 Christian Urban directory re-arrangement
less more (0) tip