haftmann [Thu, 30 Sep 2010 07:34:06 +0200] rev 39792
merged
haftmann [Wed, 29 Sep 2010 15:28:29 +0200] rev 39791
redundancy check: drop trailing Var arguments (avoids eta problems with equations)
wenzelm [Wed, 29 Sep 2010 17:59:20 +0200] rev 39790
merged
bulwahn [Wed, 29 Sep 2010 11:55:08 +0200] rev 39789
removing obsolete distinction between prod_case and other case expressions after merging of split and prod_case (d3daea901123) in predicate compiler
bulwahn [Wed, 29 Sep 2010 11:36:16 +0200] rev 39788
merged
bulwahn [Wed, 29 Sep 2010 10:33:15 +0200] rev 39787
adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
bulwahn [Wed, 29 Sep 2010 10:33:15 +0200] rev 39786
added test case for predicate arguments in higher-order argument position
bulwahn [Wed, 29 Sep 2010 10:33:15 +0200] rev 39785
improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn [Wed, 29 Sep 2010 10:33:15 +0200] rev 39784
added a test case to Predicate_Compile_Tests
bulwahn [Wed, 29 Sep 2010 10:33:14 +0200] rev 39783
putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal
krauss [Wed, 29 Sep 2010 11:02:24 +0200] rev 39782
backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).
haftmann [Wed, 29 Sep 2010 10:05:44 +0200] rev 39781
scala is reserved identifier
haftmann [Wed, 29 Sep 2010 09:21:26 +0200] rev 39780
platform-sensitive contrib paths for ghc, ocaml
haftmann [Wed, 29 Sep 2010 09:08:01 +0200] rev 39779
fact listsum now names listsum_foldl
haftmann [Wed, 29 Sep 2010 09:08:00 +0200] rev 39778
delete code lemma explicitly
haftmann [Wed, 29 Sep 2010 09:07:58 +0200] rev 39777
moved old_primrec source to nominal package, where it is still used
haftmann [Tue, 28 Sep 2010 15:39:59 +0200] rev 39776
dropped old primrec package
haftmann [Tue, 28 Sep 2010 15:34:47 +0200] rev 39775
merged
haftmann [Tue, 28 Sep 2010 15:21:45 +0200] rev 39774
localized listsum
haftmann [Tue, 28 Sep 2010 15:21:45 +0200] rev 39773
lemma listsum_conv_fold
haftmann [Tue, 28 Sep 2010 15:34:30 +0200] rev 39772
merged
haftmann [Tue, 28 Sep 2010 15:33:56 +0200] rev 39771
NEWS
haftmann [Tue, 28 Sep 2010 15:32:59 +0200] rev 39770
dropped syntax for old primrec package
haftmann [Tue, 28 Sep 2010 15:31:10 +0200] rev 39769
modernized session
bulwahn [Tue, 28 Sep 2010 13:44:06 +0200] rev 39768
merged
bulwahn [Tue, 28 Sep 2010 11:59:58 +0200] rev 39767
using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof
bulwahn [Tue, 28 Sep 2010 11:59:57 +0200] rev 39766
avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead
bulwahn [Tue, 28 Sep 2010 11:59:53 +0200] rev 39765
adding test case for interpretation of arguments that are predicates simply as input
bulwahn [Tue, 28 Sep 2010 11:59:52 +0200] rev 39764
only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input
bulwahn [Tue, 28 Sep 2010 11:59:51 +0200] rev 39763
weakening check for higher-order relations, but adding check for consistent modes
bulwahn [Tue, 28 Sep 2010 11:59:51 +0200] rev 39762
handling higher-order relations in output terms; improving proof procedure; added test case
bulwahn [Tue, 28 Sep 2010 11:59:50 +0200] rev 39761
renaming use_random to use_generators in the predicate compiler
bulwahn [Tue, 28 Sep 2010 11:59:48 +0200] rev 39760
fixed a typo that caused the preference of non-random modes to be ignored
haftmann [Tue, 28 Sep 2010 12:48:05 +0200] rev 39759
merged
haftmann [Tue, 28 Sep 2010 12:47:55 +0200] rev 39758
modernized primrecs
haftmann [Tue, 28 Sep 2010 12:47:55 +0200] rev 39757
modernized session
krauss [Tue, 28 Sep 2010 12:34:41 +0200] rev 39756
consolidated tupled_lambda; moved to structure HOLogic
haftmann [Tue, 28 Sep 2010 12:10:37 +0200] rev 39755
added dependency to base image to ensure that the doc test actually rebuilds the tutorial
krauss [Tue, 28 Sep 2010 09:54:07 +0200] rev 39754
no longer declare .psimps rules as [simp].
This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.
krauss [Tue, 28 Sep 2010 09:43:13 +0200] rev 39753
added dependency to base images to ensure that the doc test actually rebuilds the tutorials
krauss [Tue, 28 Sep 2010 09:34:20 +0200] rev 39752
removed unnecessary reference poking (cf. f45d332a90e3)
haftmann [Tue, 28 Sep 2010 09:17:33 +0200] rev 39751
merged
haftmann [Tue, 28 Sep 2010 09:14:37 +0200] rev 39750
consider quick_and_dirty option before loading theory
krauss [Tue, 28 Sep 2010 08:38:20 +0200] rev 39749
dropped obsolete mk_tcl
blanchet [Tue, 28 Sep 2010 08:35:00 +0200] rev 39748
make SML/NJ happy
haftmann [Mon, 27 Sep 2010 16:32:48 +0200] rev 39747
merged
haftmann [Mon, 27 Sep 2010 16:27:32 +0200] rev 39746
combine quote and typewriter tag; typewriter considers isa@parindent
haftmann [Mon, 27 Sep 2010 16:27:31 +0200] rev 39745
combine quote and typewriter/tt tag