src/HOL/NanoJava/Equivalence.thy
Sat, 14 Jun 2008 23:19:51 +0200 wenzelm proper context for tactics derived from res_inst_tac;
Wed, 11 Jul 2007 11:28:13 +0200 berghofe Adapted to new inductive definition package.
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Fri, 29 Aug 2003 15:19:02 +0200 ballarin Methods rule_tac etc support static (Isar) contexts.
Mon, 25 Feb 2002 18:02:22 +0100 oheimb Clarification wrt. use of polymorphic variants of Hoare logic rules
Mon, 14 Jan 2002 00:16:43 +0100 oheimb cosmetics
Mon, 17 Dec 2001 14:23:10 +0100 nipkow mods due to mor powerful simprocs for 1-point rules (quantifier1).
less more (0) -10 -8 tip