2009-10-25 chaieb 2009-10-25 Multivariate polynomials library over fields
2009-10-25 chaieb 2009-10-25 A theory of polynomials based on lists
2009-10-25 chaieb 2009-10-25 Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
2009-10-25 wenzelm 2009-10-25 merged
2009-10-24 bulwahn 2009-10-24 further changes due to the previous merge in the predicate compiler
2009-10-24 wenzelm 2009-10-24 merge -- imported from bulwahn d759e2728188;
2009-10-24 bulwahn 2009-10-24 removed tuple functions from the predicate compiler
2009-10-24 bulwahn 2009-10-24 improving the compilation with higher-order arguments in the predicate compiler
2009-10-24 bulwahn 2009-10-24 now the predicate compilere handles the predicate without introduction rules better as before
2009-10-24 bulwahn 2009-10-24 removed dead code; added examples
2009-10-24 bulwahn 2009-10-24 removed obsolete GeneratorPrem; clean-up after modularization; tuned
2009-10-24 bulwahn 2009-10-24 modularized the compilation in the predicate compiler
2009-10-24 bulwahn 2009-10-24 adapted parser for options in the predicate compiler
2009-10-24 bulwahn 2009-10-24 modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples
2009-10-24 bulwahn 2009-10-24 cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
2009-10-24 bulwahn 2009-10-24 added skip_proof option; playing with compilation of depth-limited predicates
2009-10-24 bulwahn 2009-10-24 reinvestigating the compilation of the random computation in the predicate compiler
2009-10-24 bulwahn 2009-10-24 added option to generate random values to values command in the predicate compiler
2009-10-24 bulwahn 2009-10-24 commented out the random generator compilation in the example file
2009-10-24 bulwahn 2009-10-24 added option to execute depth-limited computations for the values command in the predicate compiler
2009-10-24 bulwahn 2009-10-24 renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
2009-10-24 bulwahn 2009-10-24 simplified and improved compilation of depth-limited search in the predicate compiler
2009-10-24 bulwahn 2009-10-24 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
2009-10-24 bulwahn 2009-10-24 removed unnecessary argument rpred in code_pred function
2009-10-24 bulwahn 2009-10-24 added option show_mode_inference; added splitting of conjunctions in expand_tuples
2009-10-24 bulwahn 2009-10-24 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
2009-10-24 bulwahn 2009-10-24 further cleaning up
2009-10-24 bulwahn 2009-10-24 added option show_proof_trace
2009-10-24 bulwahn 2009-10-24 importing of polymorphic introduction rules with different schematic variable names
2009-10-24 bulwahn 2009-10-24 added option show_intermediate_results
2009-10-24 bulwahn 2009-10-24 continued cleaning up; moved tuple expanding to core
2009-10-24 bulwahn 2009-10-24 cleaned up debugging messages; added options to code_pred command
2009-10-24 bulwahn 2009-10-24 added first support for higher-order function translation
2009-10-24 bulwahn 2009-10-24 added to process higher-order arguments by adding new constants
2009-10-24 bulwahn 2009-10-24 cleaned up
2009-10-24 bulwahn 2009-10-24 added theory with alternative definitions for the predicate compiler; cleaned up examples
2009-10-24 bulwahn 2009-10-24 importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first
2009-10-24 bulwahn 2009-10-24 higher-order arguments in different rules are fixed to one name in the predicate compiler
2009-10-24 bulwahn 2009-10-24 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
2009-10-24 bulwahn 2009-10-24 changed proof method to handle widen predicate in JinjaThreads
2009-10-24 bulwahn 2009-10-24 added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
2009-10-24 bulwahn 2009-10-24 processing of tuples in introduction rules
2009-10-24 bulwahn 2009-10-24 added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
2009-10-24 bulwahn 2009-10-24 developing an executable the operator
2009-10-24 bulwahn 2009-10-24 generalizing singleton with a default value
2009-10-24 bulwahn 2009-10-24 changed elimination preprocessing due to an error with a JinjaThread predicate
2009-10-24 bulwahn 2009-10-24 added test for higher-order function inductification; added debug messages
2009-10-24 bulwahn 2009-10-24 added filtering of case constants in the definition retrieval of the predicate compiler
2009-10-24 bulwahn 2009-10-24 extended core of predicate compiler to expand tuples in introduction rules
2009-10-24 bulwahn 2009-10-24 added tupled versions of examples for the predicate compiler
2009-10-24 bulwahn 2009-10-24 moved meta_fun_cong lemma into ML-file; tuned
2009-10-25 wenzelm 2009-10-25 merged
2009-10-25 wenzelm 2009-10-25 adapted Function_Lib (cf. b8cdd3d73022);
2009-10-24 krauss 2009-10-24 configuration flag "partials"
2009-10-23 krauss 2009-10-23 renamed auto_term.ML -> relation.ML
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-10-23 krauss 2009-10-23 renamed FundefDatatype -> Function_Fun
2009-10-24 wenzelm 2009-10-24 maintain position of formal entities via name space;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;