| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2024 16:55:16 +0100 |
wenzelm |
tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 09:55:22 +0100 |
desharna |
added lemmas IMGU_subst_domain_subset and IMGU_range_vars_subset
|
file |
diff |
annotate
|
| Fri, 01 Jul 2022 11:44:06 +0200 |
desharna |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 29 Jun 2022 22:33:08 +0200 |
desharna |
tuned proof
|
file |
diff |
annotate
|
| Wed, 29 Jun 2022 20:41:29 +0200 |
desharna |
added lemmas domain_comp and unify_gives_minimal_domain
|
file |
diff |
annotate
|
| Wed, 29 Jun 2022 15:36:19 +0200 |
desharna |
added definition range_vars and lemmas vars_of_subst_conv_Union, vars_of_subst_subset, range_vars_comp_subset, and unify_gives_minimal_range
|
file |
diff |
annotate
|
| Wed, 29 Jun 2022 10:13:34 +0200 |
desharna |
added definition IMGU and lemmas IMGU_iff_Idem_and_MGU and unify_computes_IMGU
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Sat, 26 Dec 2015 15:59:27 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:47:28 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 16:02:02 +0200 |
wenzelm |
prefer plain ASCII / latex over not-so-universal Unicode;
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 17:44:31 +0200 |
wenzelm |
fixed document;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed technical or trivial unused facts
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
more precise authors and comments;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
added proof of idempotence, roughly after HOL/Subst/Unify.thy
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
tuned proofs, sledgehammering overly verbose parts
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
tuned notation
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
ported some lemmas from HOL/Subst/*;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 14:46:28 +0100 |
bulwahn |
removing obselete Id comments from HOL/ex theories
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 09:54:07 +0200 |
krauss |
no longer declare .psimps rules as [simp].
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 21 Apr 2009 09:53:31 +0200 |
krauss |
tuned proof
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 11:25:29 +0200 |
wenzelm |
induct: proper separation of initial and terminal step;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:54:03 +0200 |
berghofe |
Renamed accessible part for predicates to accp.
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:47 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:30 +0200 |
haftmann |
fixed text
|
file |
diff |
annotate
|
| Thu, 17 May 2007 22:33:41 +0200 |
krauss |
Added unification case study (using new function package)
|
file |
diff |
annotate
|