cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names

added skip_proof option; playing with compilation of depth-limited predicates

reinvestigating the compilation of the random computation in the predicate compiler

added option to generate random values to values command in the predicate compiler

commented out the random generator compilation in the example file

added option to execute depth-limited computations for the values command in the predicate compiler

renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler

simplified and improved compilation of depth-limited search in the predicate compiler

moved argument expected_modes into options; improved mode check to only check mode of the named predicate

removed unnecessary argument rpred in code_pred function

added option show_mode_inference; added splitting of conjunctions in expand_tuples

changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned

further cleaning up

added option show_proof_trace

importing of polymorphic introduction rules with different schematic variable names

added option show_intermediate_results

continued cleaning up; moved tuple expanding to core

cleaned up debugging messages; added options to code_pred command

added first support for higher-order function translation

added to process higher-order arguments by adding new constants

cleaned up

added theory with alternative definitions for the predicate compiler; cleaned up examples

importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first

higher-order arguments in different rules are fixed to one name in the predicate compiler

changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned

changed proof method to handle widen predicate in JinjaThreads

added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex

processing of tuples in introduction rules

added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions

developing an executable the operator

generalizing singleton with a default value

changed elimination preprocessing due to an error with a JinjaThread predicate

added test for higher-order function inductification; added debug messages

added filtering of case constants in the definition retrieval of the predicate compiler

extended core of predicate compiler to expand tuples in introduction rules

added tupled versions of examples for the predicate compiler

moved meta_fun_cong lemma into ML-file; tuned

merged

adapted Function_Lib (cf. b8cdd3d73022);

configuration flag "partials"

renamed auto_term.ML -> relation.ML

function package: more standard names for structures and files

renamed FundefDatatype -> Function_Fun

maintain position of formal entities via name space;

maintain explicit name space kind; export Name_Space.the_entry; tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; simplified messages;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; fully authentic merge;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

maintain abstract entry, with position, identity etc.; declare/define: explicit indication of strictness; merge_tables/join_tables: disallow duplicates based on entry identity;

tuned message;

import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);

markup for formal entities, with "def" or "ref" occurrences;

handle Sorts.CLASS_ERROR instead of arbitrary exceptions;

reactivated isatest on macbroy6 -- 3h later to avoid overlap with backup daemon;

merged

turned off old quickcheck

pat_completeness gets its own file

ignore error messages produced by ATPs

merged