Fri, 28 Sep 2007 10:29:35 +0200 - add_inductive_i now takes typ instead of typ option as argument
berghofe [Fri, 28 Sep 2007 10:29:35 +0200] rev 24744
- add_inductive_i now takes typ instead of typ option as argument - close_rule is now applied before expanding abbreviations - rulify applies norm_hhf again
Thu, 27 Sep 2007 17:57:12 +0200 proper handling of chained facts;
wenzelm [Thu, 27 Sep 2007 17:57:12 +0200] rev 24743
proper handling of chained facts;
Thu, 27 Sep 2007 17:55:28 +0200 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson [Thu, 27 Sep 2007 17:55:28 +0200] rev 24742
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
Thu, 27 Sep 2007 17:28:05 +0200 Fixed setup of transitivity reasoner (function decomp).
ballarin [Thu, 27 Sep 2007 17:28:05 +0200] rev 24741
Fixed setup of transitivity reasoner (function decomp).
Thu, 27 Sep 2007 17:22:15 +0200 some more simultaneous use_thys;
wenzelm [Thu, 27 Sep 2007 17:22:15 +0200] rev 24740
some more simultaneous use_thys;
Thu, 27 Sep 2007 11:46:05 +0200 read: explicit treatment of scanner failure;
wenzelm [Thu, 27 Sep 2007 11:46:05 +0200] rev 24739
read: explicit treatment of scanner failure;
Wed, 26 Sep 2007 22:38:11 +0200 tuned;
wenzelm [Wed, 26 Sep 2007 22:38:11 +0200] rev 24738
tuned;
Wed, 26 Sep 2007 22:28:00 +0200 tuned;
wenzelm [Wed, 26 Sep 2007 22:28:00 +0200] rev 24737
tuned;
Wed, 26 Sep 2007 22:27:44 +0200 tuned;
wenzelm [Wed, 26 Sep 2007 22:27:44 +0200] rev 24736
tuned;
Wed, 26 Sep 2007 22:21:05 +0200 * Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm [Wed, 26 Sep 2007 22:21:05 +0200] rev 24735
* Pure/Isar: unified specification syntax admits type inference and dummy patterns; print mode: no_abbrevs;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip