don't hide constant forever, since it may appear in some 'primcorec'-generated theorems

tuning

HOL-IMP fastness

merged, resolving some conflicts;

eliminated hard tabs (assuming tab-width=2);

more platform notes;

tuned whitespace;

removed odd comments -- inferred types are shown by Prover IDE;

maintain blob edits within history, which is important for Snapshot.convert/revert;

more accurate eq_content;

clarified message_positions: cover alt_id as well; tuned;

maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;

common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content); more informative type Blob, to allow markup reports;

tuned signature;

report (but ignore) markup within auxiliary files;

merged

make integer_of_char and char_of_integer work with NBE and code_simp

make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals

[mq]: news

remove hidden fact about hidden constant from code generator setup

for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'

compile

updated certificates

tuned message

tabled, v.: postpone consideration of

adapted to renaming of 'Projl' and 'Projr'

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'

adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'

renamed 'nat_{case,rec}' to '{case,rec}_nat'

renamed '{prod,sum,bool,unit}_case' to 'case_...'

adapted theories to '{case,rec}_{list,option}' names

avoid old 'prod.simps' -- better be more specific

repaired hard-coded constant names

killed 'rep_compat' option

made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'

use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture

use right local theory -- shows up when 'no_discs_sels' is set

compatibility names

use new selector support to define 'the', 'hd', 'tl'

transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'

avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'

tuned code

more 'ctr_sugar' modernization

tuning

ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2

updated docs

generate 'fundec_cong' attribute for new-style (co)datatypes * * * compile

got rid of dynamic scoping the easy way

removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)

more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's

se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets

have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)

Mac OS X Lion (macbroy6) is baseline for portable executables; fringe platforms are unsupported;

"no_memory" option for the simplifier trace to bypass memoization

tuned

merged

seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;

make triple-sure that the future scheduler is properly shutdown (see also 702278df3b57);

discontinued axiomatic 'classes', 'classrel', 'arities';

updated keywords;

more explicit axiomatization;

prefer vacuous definitional type classes over axiomatic ones;

more explicit axiomatization;

prefer vacuous definitional type classes over axiomatic ones;

comments;

removed rotten code;

more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example: lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))" using [[simp_depth_limit = 1]] apply simp oops

merged

improved lin.arith. for terms involving division

restoring ancient string_classes option

method names in instance declarations are always unqualified

dropped legacy finally

tidied messy proofs

minimal document;

removed junk;

merged

check scalable fonts;

do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super fonts, which also provide underscore for non-tt font;

yet another attempt at actual underscore; enforce scalable fonts for T1 encoding;

build up preprocessing context only once

tuned

disabled counterexample output for now; confusing because often incorrect

more indexing

merged

indexed document

Simplified some proofs, deleting a lot of strange unused material at the end of the theory.

fight spurious nitpick timeouts

reverted a87e49f4336d -- overwriting of data entries yields to merge problems later

more docs

more docs

docs

tidied

docs

docs about registering a BNF

merged

indexed document

allow multiple registration of the same type, the last wins

fixed problem (?) by deleting "thm" line

try right bunch of methods

don't waste time with old-style 'case's that don't have the required theorems

expand 'split' in direct corecursion as well

tuning

adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas

merge

properly massage 'if's / 'case's etc. under lambdas

Merge

Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.

fixed handling of 'split'

made SML/NJ happy

agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention

more exception cleanup + more liberal compressions of steps that timed out

tuned code to avoid noncanonical (and risky) exception handling

got rid of indices

corrected wrong 'meth :: _' pattern maching + tuned code

more generous Isar proof compression -- try to remove failing steps

tweaked handling of 'hopeless' methods

do a second phase of proof compression after minimization

don't give up on hopeless proof methods -- they can become hopeful again

tuned code

tuned slack

split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)

removal of "back", etc.

Restoration of Pocklington.thy. Tidying.

tuned latex

tuned latex

tuned

started index

interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state