#
6ce8882b |
|
14-Mar-2019 |
wenzelm <none@none> |
more specific keyword kinds;
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
7d86104c |
|
10-Jan-2016 |
kleing <none@none> |
print_record: diagnostic printing of record definitions
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
1ba740de |
|
02-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' in 'Main'
|
#
ddcfa175 |
|
25-Apr-2014 |
wenzelm <none@none> |
modernized theory setup;
|
#
3d1cf75b |
|
11-Mar-2014 |
blanchet <none@none> |
moved 'Quickcheck_Narrowing' further down the theory graph
|
#
beb8c069 |
|
11-Mar-2014 |
blanchet <none@none> |
make it possible to load Quickcheck exhaustive & narrowing in parallel
|
#
9e021ec0 |
|
20-Jan-2014 |
blanchet <none@none> |
tuning
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
fa22b8b3 |
|
13-Feb-2013 |
haftmann <none@none> |
abandoned theory Plain --HG-- extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
4828b4bc |
|
08-May-2012 |
bulwahn <none@none> |
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
f376a86c |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
d5ad5bb2 |
|
09-Jun-2011 |
bulwahn <none@none> |
adding theory Quickcheck_Narrowing to HOL-Main image
|
#
84682e48 |
|
05-May-2011 |
bulwahn <none@none> |
adding creation of exhaustive generators for records; simplifying dependencies in Main theory
|
#
adfe6cf9 |
|
17-Dec-2010 |
wenzelm <none@none> |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
#
8f600bf4 |
|
18-Aug-2010 |
haftmann <none@none> |
removed separate quickcheck_record module
|
#
4e6f4b16 |
|
17-Aug-2010 |
haftmann <none@none> |
dropped make_/dest_ naming convention
|
#
0a1ab8db |
|
17-Aug-2010 |
haftmann <none@none> |
eliminated typecopy interpretation
|
#
7f9e862b |
|
12-Aug-2010 |
haftmann <none@none> |
moved Record.thy from session Plain to Main; avoid variable name acc
|
#
82fe7ca2 |
|
16-Apr-2010 |
wenzelm <none@none> |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
#
843e6e8f |
|
16-Feb-2010 |
wenzelm <none@none> |
simplified/clarified record translations;
|
#
e8949437 |
|
16-Feb-2010 |
wenzelm <none@none> |
moved generic update_name to Pure syntax -- not specific to HOL/record;
|
#
38046233 |
|
16-Feb-2010 |
wenzelm <none@none> |
tuned;
|
#
3c84f1b2 |
|
15-Feb-2010 |
wenzelm <none@none> |
tuned document;
|
#
1b4000a0 |
|
21-Dec-2009 |
haftmann <none@none> |
prefer prefix "iso" over potentially misleading "is"; tuned
|
#
4e753dd2 |
|
10-Nov-2009 |
haftmann <none@none> |
substantial simplification restores code generation
|
#
dff346e8 |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated dead code, redundant bindings and parameters; use === term operator, which is defined here; handle Type.TYPE_MATCH, not arbitrary exceptions; misc tuning and simplification;
|
#
e90e24ba |
|
29-Sep-2009 |
wenzelm <none@none> |
replaced meta_iffD2 by existing Drule.equal_elim_rule2; replaced SymSymTab by existing Symreltab; more antiquotations; eliminated old-style Library.foldl, Library.foldl_map; tuned;
|
#
44e0a68c |
|
29-Sep-2009 |
wenzelm <none@none> |
tuned header;
|
#
783117e0 |
|
27-Sep-2009 |
Thomas Sewell <tsewell@nicta.com.au> |
Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.
|
#
e8e0e269 |
|
23-Sep-2009 |
tsewell@rubicon.NSW.bigpond.net.au <tsewell@rubicon.NSW.bigpond.net.au> |
Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.
|
#
611fbb19 |
|
10-Sep-2009 |
Thomas Sewell <tsewell@nicta.com.au> |
Simplification of various aspects of the IsTuple component of the new record package. Extensive documentation added in IsTuple.thy - it should now be possible to figure out what's going on from the sources supplied.
|
#
83281e24 |
|
09-Sep-2009 |
Thomas Sewell <tsewell@nicta.com.au> |
Record patch imported and working.
|
#
6aedf37f |
|
26-Aug-2009 |
tsewell@rubicon.NSW.bigpond.net.au <tsewell@rubicon.NSW.bigpond.net.au> |
Initial attempt at porting record update to repository Isabelle.
|
#
91b337ca |
|
19-Jun-2009 |
haftmann <none@none> |
discontinued ancient tradition to suffix certain ML module names with "_package" --HG-- rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML
|
#
8ce44432 |
|
19-Dec-2007 |
schirmer <none@none> |
replaced K_record by lambda term %x. c
|
#
fd68e116 |
|
26-Apr-2007 |
wenzelm <none@none> |
added header;
|
#
b467bcb2 |
|
20-Apr-2007 |
haftmann <none@none> |
reverted to classical syntax for K_record
|
#
167fea11 |
|
20-Apr-2007 |
haftmann <none@none> |
Isar definitions are now added explicitly to code theorem table
|
#
9cddea71 |
|
07-Nov-2006 |
schirmer <none@none> |
field-update in records is generalised to take a function on the field rather than the new value.
|
#
53919e03 |
|
21-Oct-2005 |
wenzelm <none@none> |
avoid home-grown meta_allE;
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
a06ec4a7 |
|
30-May-2005 |
wenzelm <none@none> |
tuned;
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
f8aaca33 |
|
04-May-2004 |
schirmer <none@none> |
tuned;
|
#
53e6b773 |
|
03-May-2004 |
schirmer <none@none> |
reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.
|
#
3401c391 |
|
29-Jun-2003 |
berghofe <none@none> |
Added split_paired_All rule for splitting variables bound by object-level universal quantifiers.
|
#
9b541a1e |
|
24-Jul-2002 |
wenzelm <none@none> |
simplified locale predicates;
|
#
34b3aa3b |
|
23-Jul-2002 |
wenzelm <none@none> |
predicate defs via locales;
|
#
c3726d43 |
|
26-Oct-2001 |
wenzelm <none@none> |
removed "more" class;
|
#
6424d125 |
|
18-Oct-2001 |
wenzelm <none@none> |
tuned;
|
#
46de09d0 |
|
18-Oct-2001 |
wenzelm <none@none> |
proper setup for abstract product types;
|
#
27c8f95d |
|
17-Oct-2001 |
wenzelm <none@none> |
abstract product types;
|
#
b6a293dd |
|
08-Aug-2001 |
wenzelm <none@none> |
_constify;
|
#
12669d66 |
|
07-Aug-2001 |
wenzelm <none@none> |
fix problem with user translations by making field names appear as consts;
|
#
12341a34 |
|
11-Dec-2000 |
wenzelm <none@none> |
added "_update_name" and parse_translation;
|
#
1af90e23 |
|
25-Oct-2000 |
wenzelm <none@none> |
more "xsymbols" syntax;
|
#
fefe5619 |
|
23-Oct-2000 |
wenzelm <none@none> |
intro_classes by default;
|
#
ffe1d863 |
|
27-Sep-2000 |
wenzelm <none@none> |
more symbolic syntax (currently "input");
|
#
66da0583 |
|
29-Aug-2000 |
wenzelm <none@none> |
\<dots> syntax;
|
#
21fe8688 |
|
25-Aug-1999 |
wenzelm <none@none> |
proper bootstrap of HOL theory and packages;
|
#
9d583abe |
|
22-Oct-1998 |
wenzelm <none@none> |
tuned block indent;
|
#
64159cf9 |
|
20-Oct-1998 |
wenzelm <none@none> |
Datatype instead of Prod;
|
#
d638127a |
|
28-Jul-1998 |
wenzelm <none@none> |
removed global_names flag;
|
#
1824f129 |
|
24-Jul-1998 |
wenzelm <none@none> |
added type and update syntax;
|
#
c044ae49 |
|
12-Jun-1998 |
wenzelm <none@none> |
changed {: :} syntax to (| |);
|
#
138c3cb2 |
|
29-Apr-1998 |
wenzelm <none@none> |
Extensible records with structural subtyping in HOL. See Tools/record_package.ML for the actual implementation.
|