1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
% -----------------------------------------------------------------------------
% (C) Altran Praxis Limited
% -----------------------------------------------------------------------------
%
% The SPARK toolset is free software; you can redistribute it and/or modify it
% under terms of the GNU General Public License as published by the Free
% Software Foundation; either version 3, or (at your option) any later
% version. The SPARK toolset is distributed in the hope that it will be
% useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
% Public License for more details. You should have received a copy of the GNU
% General Public License distributed with the SPARK toolset; see file
% COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
% the license.
%
% =============================================================================
:- dynamic(abandon_search/0).
:- dynamic(all_done/1).
:- dynamic(bad_rulefile/0).
:- dynamic(banned_rule/2).
:- dynamic(case/3).
:- dynamic(cmd_line_command_log/1).
:- dynamic(cmd_line_filename/1).
:- dynamic(cmd_line_proof_log/1).
:- dynamic(command_arg/2).
:- dynamic(command_log_filename/1).
:- dynamic(con/1).
:- dynamic(conc/2).
:- dynamic(conc_to_replace/1).
:- dynamic(could_infer/1).
:- dynamic(could_not_infer/1).
:- dynamic(csvfile_name/1).
:- dynamic(current_record_field_number/1).
:- dynamic(current_root/2).
:- dynamic(current_sat_goal/1).
:- dynamic(current_vc/2).
:- dynamic(current_vc_no/1).
:- dynamic(deleted/1).
:- dynamic(deleted_hyp/2).
:- dynamic(do_do_newvc/0).
:- dynamic(do_not_issue_failure_message/0).
:- dynamic(done__proof_log/0).
:- dynamic(done__resume/0).
:- dynamic(enumeration/2).
:- dynamic(fdl_file_title/1).
:- dynamic(fdlfile_name/1).
:- dynamic(forgotten/1).
:- dynamic(function/3).
:- dynamic(function_template/3).
:- dynamic(hn/1).
:- dynamic(hyp/2).
:- dynamic(hyp_to_replace/1).
:- dynamic(in_declare_command/0).
:- dynamic(inf_match/0).
:- dynamic(ini_file_consult/1).
:- dynamic(inst_case/4).
:- dynamic(inst_form/3).
:- dynamic(inst_saved_vc/3).
:- dynamic(inst_subgoal_formula/5).
:- dynamic(is_vc/1).
:- dynamic(is_true_vc/2).
:- dynamic(logfact/2).
:- dynamic(logfile_name/1).
:- dynamic(logged_rule_match/3).
:- dynamic(mk__function_name/3).
:- dynamic(newsub/1).
:- dynamic(num_matches/1).
:- dynamic(numsubs/1).
:- dynamic(occstoreplace/1).
:- dynamic(on_case/3).
:- dynamic(on_filename/1).
:- dynamic(pattern/1).
:- dynamic(perform_script_file/1).
:- dynamic(pos_newsub/1).
:- dynamic(posslog/2).
:- dynamic(previous_character/1).
:- dynamic(proved_for_case/2).
:- dynamic(qbindingname/2).
:- dynamic(qualifier_prefix/1).
:- dynamic(qvar/1).
:- dynamic(recent_save_command_issued/0).
:- dynamic(record_function/6).
:- dynamic(rep_working_on/3).
:- dynamic(replace_all_expr_type/1).
:- dynamic(required_sub/1).
:- dynamic(rule_applied/1).
:- dynamic(ruleused/1).
:- dynamic(ruleused_this_session/1).
:- dynamic(satisfies/2).
:- dynamic(saved_vc/2).
:- dynamic(search_count/1).
:- dynamic(spade_checker_prefix/1).
:- dynamic(spade_chkhelp_prefix/1).
:- dynamic(spark_enabled/0).
:- dynamic(stage_num/1).
:- dynamic(status/1).
:- dynamic(sub/1).
:- dynamic(subgoal_formula/4).
:- dynamic(temp_del_hyp/2).
:- dynamic(tidied_subs/1).
:- dynamic(time_for_new_vc/0).
:- dynamic(toplevel_execute/2).
:- dynamic(totally_specified_replace/0).
:- dynamic(trying_a_replace_all/0).
:- dynamic(tv_cmd_buffer/1).
:- dynamic(tv_depth/1).
:- dynamic(tv_expr/2).
:- dynamic(tv_trace/1).
:- dynamic(twiddles_conversion/2).
:- dynamic(type/2).
:- dynamic(type_alias/2).
:- dynamic(type_classification_done/0).
:- dynamic(type_classification/2).
:- dynamic(used/1).
:- dynamic(used_ident/2).
:- dynamic(user_rulefile/2).
:- dynamic(user_classification/4).
:- dynamic(uvar/1).
:- dynamic(var_const/3).
:- dynamic(vc/2).
:- dynamic(vcgfile_name/1).
:- dynamic(vcs_to_prove/1).
:- dynamic(vc_name/1).
:- dynamic(vcs_proved_this_session/1).
%###############################################################################
%END-OF-FILE
|
