isabelle: Graph

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

use nicer notation, following 783406dd051e;
13 months ago, by wenzelm
merged
13 months ago, by paulson
A bit more tidying
13 months ago, by paulson
more markup for syntax consts;
13 months ago, by wenzelm
clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;
13 months ago, by wenzelm
use nicer notation, following 783406dd051e;
13 months ago, by wenzelm
proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59);
13 months ago, by wenzelm
tuned: prefer notation for Pure.type;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned, following be8c0e039a5e;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;
13 months ago, by wenzelm
Some tidying
13 months ago, by paulson
merged
13 months ago, by paulson
Tidied some messy old proofs
13 months ago, by paulson
merged
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
clarified concrete syntax;
13 months ago, by wenzelm
more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";
13 months ago, by wenzelm
more concrete syntax and more checks;
13 months ago, by wenzelm
clarified signature: more operations;
13 months ago, by wenzelm
support for syntax const dependencies, with minimal integrity checks;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified markup: more uniform treatment of parse/print phase;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified markup: more uniform;
13 months ago, by wenzelm
tuned signature: separate markup vs. extern;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer configuration options via context;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned comments
13 months ago, by nipkow
merged
13 months ago, by paulson
Partial tidying of old proofs
13 months ago, by paulson
merged
13 months ago, by nipkow
new version of time_fun that works for classes; define T_length automatically now
13 months ago, by nipkow
merged
13 months ago, by paulson
revised/generalised some lemmas
13 months ago, by paulson
remove terminated jobs, even if futures do not complete;
13 months ago, by Fabian Huch
terminate jobs properly;
13 months ago, by Fabian Huch
clarified signature: eliminate clones;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
tuned: eliminate clone (with change of internal exceptions);
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned comments and whitespace (see also 589645894305);
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
proper const (see also 759bffe1d416 and b2800da9eb8a);
13 months ago, by wenzelm
tuned: inline constants;
13 months ago, by wenzelm
tuned: eliminate clone;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
prefer host that is less likely to be down;
13 months ago, by wenzelm
adapt and activate congprocs examples, following the current Simplifier implementation;
13 months ago, by wenzelm
original Congproc_Ex.thy by Norbert Schirmer: still inactive;
13 months ago, by wenzelm
provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: anticipate congprocs;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned signature (again): anticipate different kinds of procs;
13 months ago, by wenzelm
clarified context data;
13 months ago, by wenzelm
tuned: prefer canonical argument order;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: prefer canonical argument order;
13 months ago, by wenzelm
clarified signature: less redundant types;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
unused (see d12c58e12c51);
13 months ago, by wenzelm
tuned signature: support more general procedures;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;
13 months ago, by wenzelm
tuned modules;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
misc tuning and clarification: proper context, proper exception;
13 months ago, by wenzelm
tuned: eliminate odd clones;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
unused;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned proofs;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
Two little lemmas
13 months ago, by paulson
merged
13 months ago, by wenzelm
more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;
13 months ago, by wenzelm
tuned, following cdae621613da;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);
13 months ago, by wenzelm
tuned: more antiquotations;
14 months ago, by wenzelm
tuned: more abstract access to datatype typ;
14 months ago, by wenzelm
tuned (see also db120661dded);
14 months ago, by wenzelm
tuned: more antiquotations;
14 months ago, by wenzelm
tuned signature: eliminate aliases;
14 months ago, by wenzelm
removed odd clone (amending 100c0eaf63d5);
14 months ago, by wenzelm
clarified: more robust (dest_Type_name o body_type), which may fail in both parts;
14 months ago, by wenzelm
tuned: more antiquotations, more abstract access to datatype typ;
14 months ago, by wenzelm
recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);
14 months ago, by wenzelm
prefer host that is less likely to be down;
14 months ago, by wenzelm
tuned: more antiquotations, avoid re-certification;
14 months ago, by wenzelm
Rearranged a couple of theorems
14 months ago, by paulson
New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero
14 months ago, by paulson
merged
14 months ago, by paulson