more antiquotations;

simplified outer syntax setup; slightly more uniform Isabelle/ML indentation style;

chop_while replace drop_while and take_while

merged

take_while, drop_while

rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs

fixrec: rename match_cpair to match_Pair

remove code for obsolete 'fixpat' command

clean up definition of compile_pat function

rename some fixrec pattern-match compilation functions

adding example for case expressions

applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux

merged

adapting manual configuration in examples

finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)

adding option to globally limit the prolog execution

removing dead code

value uses bare compiler invocation: generated code does not contain antiquotations

updated files to recent changes

corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity

tuned

merged

redundancy check: drop trailing Var arguments (avoids eta problems with equations)

merged

removing obsolete distinction between prod_case and other case expressions after merging of split and prod_case (d3daea901123) in predicate compiler

merged

adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned

added test case for predicate arguments in higher-order argument position

improving the compilation to handle predicate arguments in higher-order argument positions

added a test case to Predicate_Compile_Tests

putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal

backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).

scala is reserved identifier

platform-sensitive contrib paths for ghc, ocaml

fact listsum now names listsum_foldl

delete code lemma explicitly

moved old_primrec source to nominal package, where it is still used

dropped old primrec package

merged

localized listsum

lemma listsum_conv_fold

merged

NEWS

dropped syntax for old primrec package

modernized session

merged

using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof

avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead

adding test case for interpretation of arguments that are predicates simply as input

only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input

weakening check for higher-order relations, but adding check for consistent modes

handling higher-order relations in output terms; improving proof procedure; added test case

renaming use_random to use_generators in the predicate compiler

fixed a typo that caused the preference of non-random modes to be ignored

merged

modernized primrecs

modernized session

consolidated tupled_lambda; moved to structure HOLogic

added dependency to base image to ensure that the doc test actually rebuilds the tutorial

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.