Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/Pure/goals.ML
2001-10-27
wenzelm
2001-10-27
impose hyps on initial goal configuration (prevents res_inst_tac problems);
file
|
diff
|
annotate
2001-10-22
wenzelm
2001-10-22
make this module appeat late in Pure; moved print_current_goals to display.ML; added quick_and_dirty_prove_goalw_cterm (from Isar/skip_proof.ML); added thm database functions (from Thy/thm_database.ML);
file
|
diff
|
annotate
2001-09-12
wenzelm
2001-09-12
result_error_default: include msg;
file
|
diff
|
annotate
2001-09-08
wenzelm
2001-09-08
result_error_default: output *single* error message;
file
|
diff
|
annotate
2000-12-29
wenzelm
2000-12-29
proper error msg;
file
|
diff
|
annotate
2000-11-17
wenzelm
2000-11-17
check result: Envir.beta_norm;
file
|
diff
|
annotate
2000-08-10
paulson
2000-08-10
the "nocheck" versions of goal functions now standardize their result
file
|
diff
|
annotate
2000-08-04
wenzelm
2000-08-04
Term.no_dummy_patterns;
file
|
diff
|
annotate
2000-05-30
wenzelm
2000-05-30
global timing flag;
file
|
diff
|
annotate
2000-05-18
wenzelm
2000-05-18
added disable_pr, enable_pr;
file
|
diff
|
annotate
2000-01-05
wenzelm
2000-01-05
TypeInfer.logicT;
file
|
diff
|
annotate
1999-10-27
oheimb
1999-10-27
reset_goals no longer empties the proof stack
file
|
diff
|
annotate
1999-09-29
wenzelm
1999-09-29
use Drule.strip_shyps_warning; removed Thm.implies_intr_shyps;
file
|
diff
|
annotate
1999-08-18
wenzelm
1999-08-18
proper writeln of begin_state;
file
|
diff
|
annotate
1999-08-17
wenzelm
1999-08-17
reset_goals;
file
|
diff
|
annotate
1999-07-22
wenzelm
1999-07-22
avoid '(0 subgoals)';
file
|
diff
|
annotate
1999-07-10
wenzelm
1999-07-10
prove_goalw_cterm_general: pass exeption;
file
|
diff
|
annotate
1999-07-07
wenzelm
1999-07-07
tuned output;
file
|
diff
|
annotate
1999-03-17
wenzelm
1999-03-17
qualify Theory.sign_of etc.;
file
|
diff
|
annotate
1999-02-03
wenzelm
1999-02-03
added Goal(w) and Export (from context.ML);
file
|
diff
|
annotate
1999-01-15
oheimb
1999-01-15
removed empty line (in case of empty begin_state marker) before Level line added printing of subgoals number in Level line
file
|
diff
|
annotate
1998-12-04
paulson
1998-12-04
better export for nested locales
file
|
diff
|
annotate
1998-11-25
wenzelm
1998-11-25
removed redirect_to_latex stuff;
file
|
diff
|
annotate
1998-10-29
wenzelm
1998-10-29
tuned current_goals_markers semantics to avoid empty lines;
file
|
diff
|
annotate
1998-10-23
paulson
1998-10-23
better reporting of "Additional hypotheses" in a locale
file
|
diff
|
annotate
1998-10-22
wenzelm
1998-10-22
support current_goals_markers ref variable for print_current_goals;
file
|
diff
|
annotate
1998-10-05
paulson
1998-10-05
Now prove_goalw_cterm never prints timing statistics
file
|
diff
|
annotate
1998-08-13
paulson
1998-08-13
Rule mk_triv_goal for making instances of triv_goal
file
|
diff
|
annotate
1998-08-04
wenzelm
1998-08-04
added export: thm -> thm; exported print_current_goals_default; locale support;
file
|
diff
|
annotate
1998-06-29
wenzelm
1998-06-29
moved actual (C)Pure theories to pure.ML;
file
|
diff
|
annotate
1998-06-17
nipkow
1998-06-17
Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
file
|
diff
|
annotate
1998-06-05
wenzelm
1998-06-05
tuned print_exn;
file
|
diff
|
annotate
1997-11-22
wenzelm
1997-11-22
fixed warning;
file
|
diff
|
annotate
1997-11-21
wenzelm
1997-11-21
changed Sequence interface (now Seq, in seq.ML);
file
|
diff
|
annotate
1997-11-12
wenzelm
1997-11-12
moved 'latex' from library.ML to goals.ML;
file
|
diff
|
annotate
1997-10-24
wenzelm
1997-10-24
Pure.thy;
file
|
diff
|
annotate
1997-10-23
wenzelm
1997-10-23
Sign.stamp_names_of;
file
|
diff
|
annotate
1997-10-13
wenzelm
1997-10-13
uses Sign.str_of_sort;
file
|
diff
|
annotate
1997-09-25
paulson
1997-09-25
Prints warnings using the "warning" function instead of "writeln"
file
|
diff
|
annotate
1997-09-11
wenzelm
1997-09-11
removed print_goals_ref (which was broken anyway);
file
|
diff
|
annotate
1997-07-18
wenzelm
1997-07-18
tuned error propagation msg;
file
|
diff
|
annotate
1997-07-18
wenzelm
1997-07-18
tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;
file
|
diff
|
annotate
1997-04-16
wenzelm
1997-04-16
Sorts.str_of_sort;
file
|
diff
|
annotate
1997-04-02
wenzelm
1997-04-02
changed signature of dummy goal from proto_pure to pure;
file
|
diff
|
annotate
1997-02-04
paulson
1997-02-04
Gradual switching to Basis Library functions nth, drop, etc.
file
|
diff
|
annotate
1997-01-17
paulson
1997-01-17
Added the prlim command
file
|
diff
|
annotate
1996-11-08
paulson
1996-11-08
Removed "standard" call from uresult, to allow specialist applications
file
|
diff
|
annotate
1996-10-24
paulson
1996-10-24
Allowing negative levels (as offsets) in prlev and choplev
file
|
diff
|
annotate
1996-08-20
paulson
1996-08-20
Added ref to allow suppression of error msgs
file
|
diff
|
annotate
1996-03-28
berghofe
1996-03-28
Added functions pr_latex and printgoal_latex which display current proof state in xdvi window
file
|
diff
|
annotate
1996-03-15
berghofe
1996-03-15
Added some functions which allow redirection of Isabelle's output
file
|
diff
|
annotate
1996-03-11
paulson
1996-03-11
Made an exception handler more specific
file
|
diff
|
annotate
1996-02-16
paulson
1996-02-16
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
file
|
diff
|
annotate
1996-01-29
clasohm
1996-01-29
inserted tabs again
file
|
diff
|
annotate
1996-01-29
clasohm
1996-01-29
removed tabs
file
|
diff
|
annotate
1995-12-22
paulson
1995-12-22
"prepare_proof" has been simplified because rewrite_rule and rewrite_goals_rule check for empty lists. The list of premises is *not* passed to Thm.compress; this was tried, but the potential storage gains seemed not to justify the cpu time required.
file
|
diff
|
annotate
1995-09-01
wenzelm
1995-09-01
adapted to new version of shyps-stuff;
file
|
diff
|
annotate
1995-08-01
wenzelm
1995-08-01
modified prepare_proof to handle shyps;
file
|
diff
|
annotate
1995-03-03
clasohm
1995-03-03
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
file
|
diff
|
annotate
1995-02-27
lcp
1995-02-27
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.
file
|
diff
|
annotate