2006-10-11 wenzelm 2006-10-11 add_defs: declare terms;
2006-10-11 wenzelm 2006-10-11 'context': demand 'begin', support local theory; removed 'undo_end', recovered 'cannot_undo'; tuned Toplevel.begin_local_theory;
2006-10-11 wenzelm 2006-10-11 removed 'undo_end', recovered 'cannot_undo';
2006-10-11 wenzelm 2006-10-11 tuned signature;
2006-10-11 haftmann 2006-10-11 minor refinements in serialization
2006-10-11 haftmann 2006-10-11 adapted to signature change
2006-10-11 haftmann 2006-10-11 slight type signature changes
2006-10-11 haftmann 2006-10-11 cleaned up HOL bootstrap
2006-10-11 haftmann 2006-10-11 abandoned findrep
2006-10-11 haftmann 2006-10-11 added code generator setup
2006-10-11 haftmann 2006-10-11 added code lemma
2006-10-11 paulson 2006-10-11 Abstraction re-use code now checks that the abstraction function can be used in the current theory.
2006-10-11 haftmann 2006-10-11 added examples for nested let
2006-10-11 haftmann 2006-10-11 added tex files to CVS
2006-10-11 wenzelm 2006-10-11 renamed body_context_node to presentation_context;
2006-10-11 wenzelm 2006-10-11 add_locale(_i): return actual result context; cert_facts: allow qualified names;
2006-10-11 wenzelm 2006-10-11 class(_i): mimic Locale.add_locale(_i); 'class': begin_local_theory;
2006-10-11 wenzelm 2006-10-11 added type global_theory -- theory or local_theory; added begin/exit_local_theory; removed theory_context; renamed body_context_node to presentation_context; removed copy (checkpoint twice instead -- avoids unrelated theories);
2006-10-11 wenzelm 2006-10-11 added begin;
2006-10-11 wenzelm 2006-10-11 added opt_begin;
2006-10-11 wenzelm 2006-10-11 added raw_theory(_result); tuned;
2006-10-11 wenzelm 2006-10-11 Toplevel.end_proof;
2006-10-11 wenzelm 2006-10-11 'end': handle local theory; 'locale': begin local theory;
2006-10-11 wenzelm 2006-10-11 undo_end/kill: handle local theory; Toplevel: generic_theory;
2006-10-11 wenzelm 2006-10-11 Toplevel: generic_theory;
2006-10-10 urbanc 2006-10-10 made some proof look more like the ones in Barendregt
2006-10-10 paulson 2006-10-10 A way to call the ATP linkup from ML scripts
2006-10-10 paulson 2006-10-10 Combinators require the theory name; added settings for SPASS
2006-10-10 haftmann 2006-10-10 stripped pointless head
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-10 haftmann 2006-10-10 added IsarAdvanced material
2006-10-10 krauss 2006-10-10 Induction rules have schematic variables again.
2006-10-10 haftmann 2006-10-10 initial draft
2006-10-10 haftmann 2006-10-10 *** empty log message ***
2006-10-10 haftmann 2006-10-10 initial draft
2006-10-10 haftmann 2006-10-10 fixed intendation
2006-10-10 haftmann 2006-10-10 cleanup basic HOL bootstrap
2006-10-10 haftmann 2006-10-10 added legacy tactic
2006-10-10 haftmann 2006-10-10 purged some ML legacy
2006-10-10 haftmann 2006-10-10 added eq_True eq_False True_implies_equals to extraction_expand
2006-10-10 haftmann 2006-10-10 no breaks for Haskell
2006-10-10 haftmann 2006-10-10 removed experimental codegen_simtype
2006-10-10 haftmann 2006-10-10 added keeping of funcgr
2006-10-10 haftmann 2006-10-10 generalized purge
2006-10-10 haftmann 2006-10-10 changed order
2006-10-10 haftmann 2006-10-10 removed quote in serialization
2006-10-10 haftmann 2006-10-10 added code_abstype
2006-10-10 haftmann 2006-10-10 added code_constsubst
2006-10-10 haftmann 2006-10-10 fixed typo
2006-10-10 haftmann 2006-10-10 added code_abstype and code_constsubst
2006-10-09 wenzelm 2006-10-09 isabelle-process: options -S, -X;
2006-10-09 wenzelm 2006-10-09 tuned;
2006-10-09 wenzelm 2006-10-09 loop: disallow exit in secure mode;
2006-10-09 wenzelm 2006-10-09 Secure.commit;
2006-10-09 wenzelm 2006-10-09 moved Context.ml_output to Output.ml_output;
2006-10-09 wenzelm 2006-10-09 Secure critical operations.
2006-10-09 wenzelm 2006-10-09 added General/secure.ML;
2006-10-09 wenzelm 2006-10-09 added option -S (secure mode);
2006-10-09 nipkow 2006-10-09 added nbe_post for delayed_if
2006-10-09 nipkow 2006-10-09 added delayed_if