2006-10-12 wenzelm 2006-10-12 Toplevel.local_theory_to_proof: proper target;
2006-10-12 wenzelm 2006-10-12 Toplevel.local_theory: proper target; removed dead code;
2006-10-12 urbanc 2006-10-12 To be consistent with "induct", I renamed "fixing" to "arbitrary". However I am not very fond of "arbitrary" - e.g. it clashes with "arbitrary" of HOL. Both Gentzen (at least in the Szabo translation) and Velleman (in How to prove it: a structured approach) use "arbitrary". Still, I wonder whether "generalising" is a good compromise?
2006-10-12 paulson 2006-10-12 Extended combinators now disabled
2006-10-12 paulson 2006-10-12 abstraction is now turned OFF...
2006-10-12 paulson 2006-10-12 Logging of theorem names to the /tmp directory now works
2006-10-12 wenzelm 2006-10-12 cc: avoid space after options;
2006-10-12 wenzelm 2006-10-12 set DYLD_LIBRARY_PATH (for Darwin);
2006-10-12 wenzelm 2006-10-12 added execute/system;
2006-10-12 wenzelm 2006-10-12 added x86-darwin;
2006-10-12 haftmann 2006-10-12 now allowing subdirectories in Doc/
2006-10-12 haftmann 2006-10-12 added makefile layer
2006-10-11 wenzelm 2006-10-11 * isabelle-process: option -S (secure mode) disables some critical operations;
2006-10-11 wenzelm 2006-10-11 increased heap size for polyml-4.9.1;
2006-10-11 wenzelm 2006-10-11 tuned Toplevel.begin_local_theory;
2006-10-11 wenzelm 2006-10-11 exit_local_theory: pass interactive flag; begin_local_theory: generic init;
2006-10-11 wenzelm 2006-10-11 exit: pass interactive flag; moved exit to local_theory.ML; tuned pretty;
2006-10-11 wenzelm 2006-10-11 added begin parser;
2006-10-11 wenzelm 2006-10-11 is_sid: disallow 'begin' keyword as identifier;
2006-10-11 wenzelm 2006-10-11 exit: pass interactive flag, toplevel result convention;
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