Mon, 12 Aug 2013 15:25:17 +0200 | blanchet | define case constant from other 'free constructor' axioms | file | diff | annotate |
Mon, 12 Aug 2013 15:25:16 +0200 | blanchet | introduced case tactics | file | diff | annotate |
Mon, 12 Aug 2013 15:25:16 +0200 | blanchet | tuning | file | diff | annotate |
Thu, 06 Jun 2013 21:22:04 +0200 | blanchet | tuning | file | diff | annotate |
Sun, 12 May 2013 13:08:23 +0200 | wenzelm | proper context; | file | diff | annotate |
Sat, 27 Apr 2013 20:50:20 +0200 | wenzelm | uniform Proof.context for hyp_subst_tac; | file | diff | annotate |
Sat, 27 Apr 2013 11:37:50 +0200 | blanchet | tuned ML and thy file names | file | diff | annotate | base |