isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

cleaned up
2009-10-24, by bulwahn
added theory with alternative definitions for the predicate compiler; cleaned up examples
2009-10-24, by bulwahn
importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first
2009-10-24, by bulwahn
higher-order arguments in different rules are fixed to one name in the predicate compiler
2009-10-24, by 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
2009-10-24, by bulwahn
changed proof method to handle widen predicate in JinjaThreads
2009-10-24, by bulwahn
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
2009-10-24, by bulwahn
processing of tuples in introduction rules
2009-10-24, by bulwahn
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, by bulwahn
developing an executable the operator
2009-10-24, by bulwahn
generalizing singleton with a default value
2009-10-24, by bulwahn
changed elimination preprocessing due to an error with a JinjaThread predicate
2009-10-24, by bulwahn
added test for higher-order function inductification; added debug messages
2009-10-24, by bulwahn
added filtering of case constants in the definition retrieval of the predicate compiler
2009-10-24, by bulwahn
extended core of predicate compiler to expand tuples in introduction rules
2009-10-24, by bulwahn
added tupled versions of examples for the predicate compiler
2009-10-24, by bulwahn
moved meta_fun_cong lemma into ML-file; tuned
2009-10-24, by bulwahn
merged
2009-10-25, by wenzelm
adapted Function_Lib (cf. b8cdd3d73022);
2009-10-25, by wenzelm
configuration flag "partials"
2009-10-24, by krauss
renamed auto_term.ML -> relation.ML
2009-10-23, by krauss
function package: more standard names for structures and files
2009-10-23, by krauss
renamed FundefDatatype -> Function_Fun
2009-10-23, by krauss
maintain position of formal entities via name space;
2009-10-24, by wenzelm
maintain explicit name space kind;
2009-10-24, by wenzelm
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24, by wenzelm
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-24, by wenzelm
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-24, by wenzelm
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-24, by wenzelm
maintain abstract entry, with position, identity etc.;
2009-10-24, by wenzelm
tuned message;
2009-10-24, by wenzelm
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
2009-10-24, by wenzelm
markup for formal entities, with "def" or "ref" occurrences;
2009-10-24, by wenzelm
handle Sorts.CLASS_ERROR instead of arbitrary exceptions;
2009-10-24, by wenzelm
reactivated isatest on macbroy6 -- 3h later to avoid overlap with backup daemon;
2009-10-23, by wenzelm
merged
2009-10-23, by haftmann
turned off old quickcheck
2009-10-23, by haftmann
pat_completeness gets its own file
2009-10-23, by krauss
ignore error messages produced by ATPs
2009-10-23, by boehmes
merged
2009-10-23, by haftmann
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)
2009-10-23, by haftmann
restored accidentally deleted submultiset
2009-10-22, by haftmann
multiset operations with canonical argument order
2009-10-22, by haftmann
arg_types_of auxiliary function; using multiset operations
2009-10-22, by haftmann
merged
2009-10-23, by haftmann
close thm derivations explicitly
2009-10-22, by haftmann
Fix a duplicate abbreviation || in etc/symbols.
2009-10-23, by tbourke
made SML/NJ happy;
2009-10-22, by wenzelm
updated session name;
2009-10-22, by wenzelm
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
2009-10-22, by wenzelm
merged
2009-10-22, by wenzelm
merged
2009-10-22, by wenzelm
merged
2009-10-21, by wenzelm
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
2009-10-21, by wenzelm
merged
2009-10-22, by wenzelm
explicit close_derivation
2009-10-22, by haftmann
merged
2009-10-22, by haftmann
map_range (and map_index) combinator
2009-10-22, by haftmann
dropped Datatype.distinct_simproc
2009-10-22, by haftmann
use Synchronized.assign to achieve actual immutable results;
2009-10-22, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle