maintain group via name space, not tags; tuned;

LocalTheory.naming_of;

begin_theory: set theory_name here;

maintain group via name space, not tags;

maintain proper Name_Space.naming, with conceal and set_group; maintain group via name space, not tags; tuned signature; tuned;

more direct access to naming; tuned signature;

Name_Space.naming: maintain group and theory_name as well; tuned;

export is_concealed; tuned;

merge_list: no exception DUP here;

merged

more uniform ISABELLE_USEDIR_OPTIONS;

make SML/NJ happy;

conceal consts via name space, not tags;

allow name space entries to be "concealed" -- via binding/naming/local_theory;

switch to polyml-5.2.1 to see if it impacts performance;

merged

Multivariate polynomials library over fields

A theory of polynomials based on lists

Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)

merged

further changes due to the previous merge in the predicate compiler

merge -- imported from bulwahn d759e2728188;

removed tuple functions from the predicate compiler

improving the compilation with higher-order arguments in the predicate compiler

now the predicate compilere handles the predicate without introduction rules better as before

removed dead code; added examples

removed obsolete GeneratorPrem; clean-up after modularization; tuned

modularized the compilation in the predicate compiler

adapted parser for options in the predicate compiler

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

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

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)

restored accidentally deleted submultiset

multiset operations with canonical argument order

arg_types_of auxiliary function; using multiset operations

merged

close thm derivations explicitly