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
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
export constdefs according to defs.ML;
21 months ago, by wenzelm
avoid spurious shyps (with vacous type variable);
21 months ago, by wenzelm
merged
21 months ago, by wenzelm
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
21 months ago, by wenzelm
clarified signature: name of standard_proof is authentic, otherwise empty;
21 months ago, by wenzelm
clarified expand_proof/expand_name: allow more detailed control via thm_header;
21 months ago, by wenzelm
option to export standardized proof terms (not scalable);
21 months ago, by wenzelm
more kinds, notably for Isabelle/MMT;
21 months ago, by wenzelm
refined proof of concept for bit operations
21 months ago, by haftmann
more lemmas
21 months ago, by haftmann
merged
21 months ago, by wenzelm
export toplevel proof similar to named PThm;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
proper protocol_message for bootstrap proofs;
21 months ago, by wenzelm
proper export of bootstrap proofs (amending a6304b4664b6);
21 months ago, by wenzelm
more robust  avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;
21 months ago, by wenzelm
proper treatment of self thm_id;
21 months ago, by wenzelm
added quickcheck setup
21 months ago, by haftmann
generalized
21 months ago, by haftmann
moved quickcheck setup to distribution
21 months ago, by haftmann
moved generic instance to distribution
21 months ago, by haftmann
clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
21 months ago, by wenzelm
turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;
21 months ago, by wenzelm
support dummy term;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
21 months ago, by wenzelm
proper Thm.transfer;
21 months ago, by wenzelm
clarified files;
21 months ago, by wenzelm
clarified proof_boxes (requires prune_proofs=false);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
more robust;
21 months ago, by wenzelm
more robust: avoid looping Lazy.force due to misinterpreted interrupt;
21 months ago, by wenzelm
more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);
21 months ago, by wenzelm
tuned  more stable type inference;
21 months ago, by wenzelm
updated to jdk11.0.4+11;
21 months ago, by wenzelm
updated to scala2.12.10;
21 months ago, by wenzelm
more support for proof terms;
21 months ago, by wenzelm
more support for proof terms;
21 months ago, by wenzelm
support for proof terms;
21 months ago, by wenzelm
clarified proof export;
21 months ago, by wenzelm
set_preproc for objectlogics with type classes;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
skip (somewhat pointless) shrink_proof more uniformly;
21 months ago, by wenzelm
apply_preproc for all proof boxes;
21 months ago, by wenzelm
cumulative errors for session partitions;
21 months ago, by wenzelm
proper guard for process_theory: ensure uniform precedence of results;
21 months ago, by wenzelm
load HOLProofs first: it introduces some extra "thm" items that are required later on;
21 months ago, by wenzelm
clarified count_file;
21 months ago, by wenzelm
clarified modules;
21 months ago, by wenzelm
more complete coverage of sessions: process_theory operation needs to handle duplicate theories;
21 months ago, by wenzelm
proper build_graph to make session selection work as in "isabelle build";
21 months ago, by wenzelm
incorporate sessions with record_proofs;
21 months ago, by wenzelm
clarified options;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
clarified "isabelle update" options  more like "isabelle dump";
21 months ago, by wenzelm
clarified treatment of base logic image;
21 months ago, by wenzelm
simplified options: always split;
21 months ago, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
tip