Sun, 25 Oct 2009 20:54:21 +0100 wenzelm maintain theory name via name space, not tags;
Sun, 25 Oct 2009 19:21:34 +0100 wenzelm name space groups are identified by serial, not serial_string;
Sun, 25 Oct 2009 19:19:41 +0100 wenzelm maintain group via name space, not tags;
Sun, 25 Oct 2009 19:19:35 +0100 wenzelm LocalTheory.naming_of;
Sun, 25 Oct 2009 19:19:29 +0100 wenzelm begin_theory: set theory_name here;
Sun, 25 Oct 2009 19:18:59 +0100 wenzelm maintain group via name space, not tags;
Sun, 25 Oct 2009 19:18:25 +0100 wenzelm maintain proper Name_Space.naming, with conceal and set_group;
Sun, 25 Oct 2009 19:17:42 +0100 wenzelm more direct access to naming;
Sun, 25 Oct 2009 19:14:46 +0100 wenzelm Name_Space.naming: maintain group and theory_name as well;
Sun, 25 Oct 2009 19:14:25 +0100 wenzelm export is_concealed;
Sun, 25 Oct 2009 19:14:11 +0100 wenzelm merge_list: no exception DUP here;
Sun, 25 Oct 2009 13:20:31 +0100 wenzelm merged
Sun, 25 Oct 2009 13:14:00 +0100 wenzelm more uniform ISABELLE_USEDIR_OPTIONS;
Sun, 25 Oct 2009 13:04:06 +0100 wenzelm make SML/NJ happy;
Sun, 25 Oct 2009 13:18:35 +0100 wenzelm conceal consts via name space, not tags;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
Sun, 25 Oct 2009 11:58:11 +0100 wenzelm switch to polyml-5.2.1 to see if it impacts performance;
Sun, 25 Oct 2009 08:57:55 +0100 chaieb merged
Sun, 25 Oct 2009 08:57:36 +0100 chaieb Multivariate polynomials library over fields
Sun, 25 Oct 2009 08:57:36 +0100 chaieb A theory of polynomials based on lists
Sun, 25 Oct 2009 08:57:35 +0100 chaieb Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
Sun, 25 Oct 2009 00:10:25 +0200 wenzelm merged
Sat, 24 Oct 2009 20:27:26 +0200 bulwahn further changes due to the previous merge in the predicate compiler
Sat, 24 Oct 2009 23:57:42 +0200 wenzelm merge -- imported from bulwahn d759e2728188;
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn removed tuple functions from the predicate compiler
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn improving the compilation with higher-order arguments in the predicate compiler
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn now the predicate compilere handles the predicate without introduction rules better as before
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn removed dead code; added examples
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn removed obsolete GeneratorPrem; clean-up after modularization; tuned
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn modularized the compilation in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn adapted parser for options in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn 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
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added skip_proof option; playing with compilation of depth-limited predicates
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn reinvestigating the compilation of the random computation in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added option to generate random values to values command in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn commented out the random generator compilation in the example file
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added option to execute depth-limited computations for the values command in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn simplified and improved compilation of depth-limited search in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn moved argument expected_modes into options; improved mode check to only check mode of the named predicate
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn removed unnecessary argument rpred in code_pred function
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added option show_mode_inference; added splitting of conjunctions in expand_tuples
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn further cleaning up
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added option show_proof_trace
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn importing of polymorphic introduction rules with different schematic variable names
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added option show_intermediate_results
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn continued cleaning up; moved tuple expanding to core
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn cleaned up debugging messages; added options to code_pred command
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added first support for higher-order function translation
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added to process higher-order arguments by adding new constants
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn cleaned up
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added theory with alternative definitions for the predicate compiler; cleaned up examples
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn higher-order arguments in different rules are fixed to one name in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn 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
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn changed proof method to handle widen predicate in JinjaThreads
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn processing of tuples in introduction rules
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip