Quot/QuotMain.thy
Mon, 07 Dec 2009 21:53:50 +0100 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 ===>
less more (0) -1 tip