adding example for case expressions

applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux

merged

adapting manual configuration in examples

finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)

adding option to globally limit the prolog execution

removing dead code

value uses bare compiler invocation: generated code does not contain antiquotations

updated files to recent changes

corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity

tuned

merged

redundancy check: drop trailing Var arguments (avoids eta problems with equations)

merged

removing obsolete distinction between prod_case and other case expressions after merging of split and prod_case (d3daea901123) in predicate compiler

merged

adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned

added test case for predicate arguments in higher-order argument position

improving the compilation to handle predicate arguments in higher-order argument positions

added a test case to Predicate_Compile_Tests

putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal

backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).

scala is reserved identifier

platform-sensitive contrib paths for ghc, ocaml

fact listsum now names listsum_foldl

delete code lemma explicitly

moved old_primrec source to nominal package, where it is still used

dropped old primrec package

merged

localized listsum

lemma listsum_conv_fold

merged

NEWS

dropped syntax for old primrec package

modernized session

merged

using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof

avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead

adding test case for interpretation of arguments that are predicates simply as input

only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input

weakening check for higher-order relations, but adding check for consistent modes

handling higher-order relations in output terms; improving proof procedure; added test case

renaming use_random to use_generators in the predicate compiler

fixed a typo that caused the preference of non-random modes to be ignored

merged

modernized primrecs

modernized session

consolidated tupled_lambda; moved to structure HOLogic

added dependency to base image to ensure that the doc test actually rebuilds the tutorial

no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.

added dependency to base images to ensure that the doc test actually rebuilds the tutorials

removed unnecessary reference poking (cf. f45d332a90e3)

merged

consider quick_and_dirty option before loading theory

dropped obsolete mk_tcl

make SML/NJ happy

merged

combine quote and typewriter tag; typewriter considers isa@parindent

combine quote and typewriter/tt tag

combine quote and typewriter tag; typewriter considers isa@parindent

combine quote and typewriter tag

CONTROL-mouse management: handle windowDeactivated as well; some workarounds to robustify html_popup;

CONTROL-mouse management: handle windowIconified; html_panel: tuned border;

basic support for message popups via HTML_Panel; more systematic CONTROL-mouse management; tuned;

tuned default perspective;

tuned README;

more defensive overview.paintComponent: avoid potential crash due to buffer change while painting;

tuned README;

more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state;

moved "auto-start" to options panel; tuned;

renamed raw output primitives to emphasize their meaning -- not to be used in user-space;

added Standard_System.unzip (for platform file-system); tuned comments;

bulk read: observe EOF protocol more carefully -- 0 counts as successful read;

tuned whitespace;

merged

lemma remdups_map_remdups

lemma remdups_list_of_dlist

merged

adopting example

adding further tracing messages; tuned

handling nested cases more elegant by requiring less new constants

merged

renamed function

rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"

comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)

remove needless flag

added hint on reference equality

treat equality on refs and arrays as primitive operation

corrected OCaml operator precedence

corrected scope of closure

merged

separate quote tag from tt tag

separate quote tag from tt tag

make SML/NJ happy

some more options to robustify posix_untar;

more efficient posix_untar -- avoid really slow java.util.zip.GZIPInputStream; misc tuning;

back to UseQuartz=true -- used to be default on Apple Java 1.5;

raw_untar.raw_execute with native cwd, to avoid cross-platform complications; more informative treatment of IOException, notably due to broken pipe;

added Standard_System.raw_untar;

some markup for inner syntax tokens;

tuned signatures and messages;

Session_Dockable: more startup controls;

simplified / clarified Session.Phase;

more precise treatment of backgrounds vs. rectangles;

tuned mk_fifo;

tuned signature;

tuned border;

more informative Session.Phase;

merged

merged

tuned schema table

tuned warning_color;

tuned error_color;

some attempts to improve visual appearance of bad text;

clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees; tuned;

updated generated file;

modernized structure Ord_List;

isatest: indicate Isabelle version;

actually handle Type.TYPE_MATCH, not arbitrary exceptions;

merged

prefer typewrite tag over raw latex environment

avoid fragile tranclp syntax; corrected resolution; corrected typo

merged

use typewriter tag instead of bare environment

dropped dead code

always add trailing newline for presentation

corrected omission

fixed small font size fore typewriter text

merged

load theory explicitly

merge

make SML/NJ happier -- temporary solution until Metis is fixed upstream

merged

being a little less strict than in 2e06dad03dd3

quotient package: respectfulness and preservation of identity.

merged

merged

removed superfluous output_typewriter from cs 65064e8f269

more idiomatic handling of latex typewriter type setting

more canonical type setting of type writer code examples

resynchronize isabelle.sty

reverted cs 5aced2f43837 -- no need for hardwired latex command here

reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter

reverted cs 07549694e2f1

shifted abstraction over imperative print mode

removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned

moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule

exporting the generic version instead of the context version in quickcheck

splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests

adding a mutual recursive example for named alternative rules for the predicate compiler

handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types

improving naming of assumptions in code_pred

adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim

handling equivalences smarter in the predicate compiler

removing duplicate rewrite rule from simpset in predicate compiler

rewriting function mk_Eval_of in predicate compiler

merged

improved and tuned external codegen tool

make SML/NJ happy

CONTRIBUTORS and NEWS

corrections and tuning

merged

merged

merged

tuned

persistent session-panel.selection;

slightly more robust EditBus plumbing wrt. Document_View/Document_Model;

permissive exit;

added Session_Dockable.session_phase label;

separate Plugin.init_model; slightly more robust initialization of Document_View/Document_Model, depending of Session.phase;

simplified Session.Phase; slightly more robust session startup; misc tuning;

tuned messages -- cf. Admin/MacOS/App1;

tuned dialog;

explicit Session.Phase indication with associated event bus; asynchronous Session.start(); synchronous Session.stop(); added Plugin.session_manager on top of basic Session; eliminated separate isabelle.activate action; misc tuning;

tuned signature;

Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;

tuned;

manage persistent syslog via Session, not Isabelle_Process; tuned;

tuned prover message categorization;

tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;

tuned message;

Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;

Snapshot.convert/revert: explicit error report to isolate sporadic crash;

make compiler doubly sure;

isabelle-process: less verbose no-commit mode;

tuned message;

tuned panel names and actions;

renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;

reactivated polyml-5.4.0 -- SVN 1214 fixes a problem with arbitrary precision arithmetic that was triggered by method "approximation" in HOL/Decision_Procs/Approximation_Ex.thy;

merged

more lists lemmas

merged

merged

tuned text

sections on @{code} and code_reflect

formal syntax diagram for code_reflect

distinguish SML and Eval explicitly

no_frees_* is subsumed by new framework mechanisms in Code_Preproc

reject term variables explicitly

avoid frees and vars in terms to be evaluated by abstracting and applying

tuned whitespace

make SML/NJ happier

more conventional conversion signature

added nbe paper

continued section abut evaluation

make SML/NJ happier

new lemma

merged

new lemmas

revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms

basic setup for Session_Dockable controls;

tuned signature;

more content for Session_Dockable;

basic support for full document rendering;

Session_Dockable: basic syslog output;

just one Session.raw_messages event bus;

more reactive handling of Isabelle_Process startup errors;

eliminated Simple_Thread shorthands that can overlap with full version;

main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;

more robust Managed_Process.kill: check after sending signal;

more robust lib/scripts/process, with explicit script/no_script mode; added general Isabelle_System.Managed_Process, with bash_output as application; tuned;

Standard_System.with_tmp_file: deleteOnExit to make double sure;

refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;

tuned whitespace;

tuned;

added Standard_System.slurp convenience; tuned;

added Simple_Thread.future convenience; tuned;

refined ML/Scala bash wrapper, based on more general lib/scripts/process;

tuned;

more robust Isabelle_System.rm_fifo: avoid external bash invocation, which might not work in JVM shutdown phase (due to Runtime.addShutdownHook);

tuned;

added Isabelle_Process.syslog; refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads; tuned;

updated keywords;

merged

merged

corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself

dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term

Pure equality is a regular cpde operation

full palette of dynamic/static value(_strict/exn)

Factored out ML into separate file