e9458b1a7a19a63aa4c179f9ab20f4d50681c168 |
|
25-Mar-2016 |
Jens Elkner <jel+git@iws.cs.uni-magdeburg.de> |
applied utils/replaceAllHeaders.sh
- all $Header$ tokens in doc comments replaced with corresponding filename |
e24ad3f655daa60ddabe690e4b11de3187996c16 |
|
22-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
moved the IO availability test into the prover and checker records |
eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7c |
|
20-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
added jedit for Isabelle proving |
2857cf346f2387af92b04a43c41e829c00664ed1 |
|
20-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
port to Isabelle2014 |
074fa38abe1cef6132877a888b080d26d96697d2 |
|
17-Jul-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
sending explicit EOT is not needed |
b161fda9df774b071a907cc9b18f0e7aee244129 |
|
17-Jul-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
added simple automatic prover based on isabelle-process |
d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488 |
|
16-Jul-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
added isabelle-process prover to avoid user interaction |
0db76fa4de562d31f829d0113500e70771f0852d |
|
27-Jun-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
changed import |
3d3889e0cefcdce9b3f43c53aaa201943ac2e895 |
|
29-Nov-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
removed lots of hlint warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18342 cec4b9c1-7d33-0410-9eda-942365e851bb |
98890889ffb2e8f6f722b00e265a211f13b5a861 |
|
01-Sep-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Added see license.txt to license field
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13959 cec4b9c1-7d33-0410-9eda-942365e851bb |
b87efd3db0d2dc41615ea28669faf80fc1b48d56 |
|
11-Aug-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Changed haddock headers and inserted empty headers for the ones missing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13857 cec4b9c1-7d33-0410-9eda-942365e851bb |
585022165936af756d04986425a0ab3b78ba98dc |
|
21-Jan-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
use Isabelle 2009 calling convention
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12993 cec4b9c1-7d33-0410-9eda-942365e851bb |
2eb18519bf2f61e04ffbe68ab06ec1e32eee07d7 |
|
09-Dec-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
only check for one proven goal
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12902 cec4b9c1-7d33-0410-9eda-942365e851bb |
90fbaf1cd73486129e26e1ac94a413550832e4d6 |
|
07-Dec-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
fixed timeout issue.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12897 cec4b9c1-7d33-0410-9eda-942365e851bb |
2f1781ab0a0a58328ef9d1ad8bda1984fd80259d |
|
10-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
only use two states proved consistent or inconsistent
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12816 cec4b9c1-7d33-0410-9eda-942365e851bb |
d1c15b86fa5f1b34ef777ff740a4bc9ae7fd0a54 |
|
03-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored consistency checker interface
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12778 cec4b9c1-7d33-0410-9eda-942365e851bb |
80c2d23821d095b55d9a547f48fc3fcdc27df405 |
|
28-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored consistency checkers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12745 cec4b9c1-7d33-0410-9eda-942365e851bb |
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3 |
|
16-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored prover stuff
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12661 cec4b9c1-7d33-0410-9eda-942365e851bb |
eee01977bc7ead7e5dba08912ff15beb33604882 |
|
27-Jan-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
only generate a proof if it is missing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11326 cec4b9c1-7d33-0410-9eda-942365e851bb |
42f38bd450a260a4494113dc89041ef9b1c5f87c |
|
27-Jan-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
only set thmProof for proper sentences
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11325 cec4b9c1-7d33-0410-9eda-942365e851bb |
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7 |
|
25-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed trailing spaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11082 cec4b9c1-7d33-0410-9eda-942365e851bb |
f094a7999dfa79cad2eb34ce15f1939c0d6b9e39 |
|
14-Nov-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactored prover interface: carry around freeness constraints
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11008 cec4b9c1-7d33-0410-9eda-942365e851bb |
433bb7cb49200f4e6c7341101da25309e423c0e2 |
|
14-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored prover template
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11005 cec4b9c1-7d33-0410-9eda-942365e851bb |
f04d7c1dac7b1dc835e63c671027455f8db17837 |
|
01-Oct-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
use prover string directly
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10755 cec4b9c1-7d33-0410-9eda-942365e851bb |
01e278bdd7dce13b9303ed3d79683d83c89d09f9 |
|
19-Aug-2008 |
Liam O'Reilly <csliam@swansea.ac.uk> |
merged Isabelle.IsaSign and Isabelle.IsaProof
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10539 cec4b9c1-7d33-0410-9eda-942365e851bb |
1d3635d5ca4cfbe47c3f1add3790f68b6c76c57d |
|
18-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
treat now metaTerms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10365 cec4b9c1-7d33-0410-9eda-942365e851bb |
c4ba3e20a432419afff01558e425e00be42871d8 |
|
15-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
added instance sentences and used Proof type
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10329 cec4b9c1-7d33-0410-9eda-942365e851bb |
b205bc86685958085af2b816c277faef3ebed52a |
|
30-Jun-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
excluded automatic simp for theorems
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10231 cec4b9c1-7d33-0410-9eda-942365e851bb |
dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9 |
|
02-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced getEnv by a safer getEnvDef
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9862 cec4b9c1-7d33-0410-9eda-942365e851bb |
9f84560989b06003d74d125ed8b8ca99a94bd165 |
|
26-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
only included 'defs' to be used by auto
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8914 cec4b9c1-7d33-0410-9eda-942365e851bb |
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0 |
|
25-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
made new module for the simplifier and added all axioms to auto proof
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8904 cec4b9c1-7d33-0410-9eda-942365e851bb |
cd0fea9ed87cf249acb7dcef2b6d3e82f308114b |
|
25-Sep-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
allowed to generate a replacement for oops
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8902 cec4b9c1-7d33-0410-9eda-942365e851bb |
1a59bc0dcee497a3ee9cfe0b357e7f3e2a78912a |
|
23-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused import
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8692 cec4b9c1-7d33-0410-9eda-942365e851bb |
0a64bfd28dff15bc93e1f7a86e0a8052e879636d |
|
23-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed getPermessions and replaced checkInFile with doesFileExist
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8691 cec4b9c1-7d33-0410-9eda-942365e851bb |
135bcb7f65991146c103e5e7599adbc49fe7359d |
|
16-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced senName with senAttr
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8627 cec4b9c1-7d33-0410-9eda-942365e851bb |
80d0480a60b409d9cf256d0a6c411dd99c672124 |
|
15-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up Logic.Prover
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8621 cec4b9c1-7d33-0410-9eda-942365e851bb |
807d5fddaa5dd8924321c73400fcf875a9ed9a9c |
|
14-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
libdir is not needed for printing Isabelle theories
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8606 cec4b9c1-7d33-0410-9eda-942365e851bb |
e1f395fef7ea8b00a675a330e5461fad35158ca5 |
|
10-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
added haddock descriptions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8319 cec4b9c1-7d33-0410-9eda-942365e851bb |
3f69b6948966979163bdfe8331c38833d5d90ecd |
|
05-Jul-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed my maintainer email
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8261 cec4b9c1-7d33-0410-9eda-942365e851bb |
cd6e5706893519bfcf24539afa252fcbed5097dd |
|
26-Jun-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* Refactoring of classes Logic, Sentences and StaticAnalysis
* Logic.Prover.ProverTemplate has now a field for the maximal sublogic
needed by a Prover/ConsChecker
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8145 cec4b9c1-7d33-0410-9eda-942365e851bb |
db6f944c6c4ca8605fa6ba215a548aa4c5ed7ecd |
|
15-Jun-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8050 cec4b9c1-7d33-0410-9eda-942365e851bb |
fd8a322d7f0f3e1bdd82217766d9c8b67f539d54 |
|
15-Jun-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
check the isDef attribute instead of the label
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8049 cec4b9c1-7d33-0410-9eda-942365e851bb |
c44c23429c72f3a709e22a18f2ed6f05fc8cc765 |
|
03-Apr-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
renamed emptyName to makeNamed
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7782 cec4b9c1-7d33-0410-9eda-942365e851bb |
65835942d66905c377fa503e0d577df5aade58fe |
|
03-Apr-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
generalized emptyName
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7775 cec4b9c1-7d33-0410-9eda-942365e851bb |
16076938607b9401efc432359077252dd0ed0d63 |
|
22-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
create thy files in current directory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7512 cec4b9c1-7d33-0410-9eda-942365e851bb |
ad270004874ce1d0697fb30d7309f180553bb315 |
|
21-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
switched to Data.Set, Data.Map and Data.Dynamic
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7491 cec4b9c1-7d33-0410-9eda-942365e851bb |
5cfeedad8c9d43f62f8e8b85ab73c0dd4e91d976 |
|
20-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved remaining todos to trac
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7481 cec4b9c1-7d33-0410-9eda-942365e851bb |
e54f9b5c61c7aa2d64474baacb76358893c93400 |
|
22-Jan-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
checked for 'simp' in axioms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7328 cec4b9c1-7d33-0410-9eda-942365e851bb |
eea4921dafc41c1e2ed3782a9cdc1a2482b79efb |
|
23-Oct-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unnecessary Isabelle term constructors
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7094 cec4b9c1-7d33-0410-9eda-942365e851bb |
f43321aca70c37a1a6fe7d463f1525ae9ebf9413 |
|
05-Sep-2006 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
Set Tactic_script back to String (in Logic.Prover), using ATPTactic_script for SoftFOL.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6920 cec4b9c1-7d33-0410-9eda-942365e851bb |
f64f3dc78de82101483fe97bf109a42ca4d59d77 |
|
29-Aug-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
preparations for the CMDLine proving interface
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6901 cec4b9c1-7d33-0410-9eda-942365e851bb |
81eaac399d69af15425d06b054e5d0331dbc132b |
|
25-Aug-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed MixfixApp constructor for an unique application representation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6892 cec4b9c1-7d33-0410-9eda-942365e851bb |
2870844cf0e81c9e2c24a7fa18cc2bdfe84d3a46 |
|
15-Aug-2006 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
* changed Tacticscript type (see in Logic.Prover)
* improved output for MathServ-based provers, now displayed with Pretty
* improved display of box "save prover configuration" in GUI.GenericATP, using Pretty functions in module GUI.PrintUtils
* added field timeUsed in GenericConfig. It should contain number of milliseconds for a prover run. Already filled in SPASS and MathServ-based provers.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6820 cec4b9c1-7d33-0410-9eda-942365e851bb |
f66307931b252b573d6fd52cf35b97114786405e |
|
14-Aug-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
keep signature for consistency
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6816 cec4b9c1-7d33-0410-9eda-942365e851bb |
3fe4d4988c6d17ce5df9b413af03944114dc5d63 |
|
28-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
refined setting simp flag
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6735 cec4b9c1-7d33-0410-9eda-942365e851bb |
c438c79d00fc438f99627e612498744bdc0d0c89 |
|
22-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
switched over to new Doc
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6478 cec4b9c1-7d33-0410-9eda-942365e851bb |
2caa469afa557120b12fea247fd2078892ab52f9 |
|
19-Apr-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
changed openProof_status
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6214 cec4b9c1-7d33-0410-9eda-942365e851bb |
5c7228df8b5c735df42d849ffde9cbb96958a849 |
|
23-Mar-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* removed field goalUsedInProof from Logic.Prover.SenStatus
* instead GoalStatus.Proved has a Parameter indicating the consistency
(similiar to the SZS Ontology)
* introduced a new StatusIndicator for Proved theorems in an inconsistent
theory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6109 cec4b9c1-7d33-0410-9eda-942365e851bb |
46b8ba7474c61b90ceb0d3a1c7fe6f4cfe9c7028 |
|
08-Mar-2006 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
patch with backup
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5927 cec4b9c1-7d33-0410-9eda-942365e851bb |
31013d9f51febd301372b8ca813d6d22e681285e |
|
14-Feb-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed duplicate dependencies
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5815 cec4b9c1-7d33-0410-9eda-942365e851bb |
b12fd4eb8134a8785f355817935d54ec7f06c1cb |
|
13-Feb-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed emptiness test for deps files
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5808 cec4b9c1-7d33-0410-9eda-942365e851bb |
724be620c516160e7d2c203999f01df4ccc53048 |
|
31-Jan-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Refactored Logic.Prover.Proof_status:
now a Record datatype with only two variants:
(1) Proof_status for goals
(2) Consistency
The status of a goal is now represented by a separate enumerated datatype:
GoalStatus
added field goalIsUsedInProof which should be True if the goal was in the
list of used formulae
other changes:
* improved display of proof details in GUI.ProofManagement
* added todo point for Isabelle.IsaProve
* Logic.Logic.Sentences demands Ord instancew for proof_tree now
so it was easier to derive the Ord instance of Proof_status automatically
* SPASS removes now the goal from the list of used axioms and stores the
derived information properly
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5750 cec4b9c1-7d33-0410-9eda-942365e851bb |
b418a0262aa84ea68de72623793361bebed51f9e |
|
16-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused bits
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5532 cec4b9c1-7d33-0410-9eda-942365e851bb |
177b47384142a17a086bf08966097e9c624d7891 |
|
16-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
made calling Isabelle more robust
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5531 cec4b9c1-7d33-0410-9eda-942365e851bb |
c97ea41501cc68e04648fbed17812eee014a89a0 |
|
15-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added consistency check of user supplied thy file
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5526 cec4b9c1-7d33-0410-9eda-942365e851bb |
4ef05f4edeb290beb89845f57156baa5298af7c4 |
|
08-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added consistency checking
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5506 cec4b9c1-7d33-0410-9eda-942365e851bb |
b6a54d7292d7a3713000847334de4316d105f40f |
|
08-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed module CreateThy
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5505 cec4b9c1-7d33-0410-9eda-942365e851bb |
ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336c |
|
07-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
simplified prover interface
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5499 cec4b9c1-7d33-0410-9eda-942365e851bb |
aa9a7405e3150b8d1caeba44af7c9e562231aff7 |
|
25-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed theory creation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5461 cec4b9c1-7d33-0410-9eda-942365e851bb |
4ab85f08ab4d473b9546948eb7fc86e5903cda81 |
|
14-Nov-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
true should be True
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5387 cec4b9c1-7d33-0410-9eda-942365e851bb |
1ac0c4de66a297fd7e345d9275f723fd83bb7bd1 |
|
10-Nov-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up and changed second VName component
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5374 cec4b9c1-7d33-0410-9eda-942365e851bb |
9603ad7198b72e812688ad7970e4eac4b553837a |
|
25-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Refactoring of ThSens, Theory, SenStatus:
* SenStatus is now parametrised over a theoremStatus, too;
it is used for structured and basic theories;
value is no longer a (Named a);
isDef, isAxiom are now fields of SenStatus, too
* ThSens is not a Set any longer it is now a Common.OrderedMap.OMap
* Theory contains now a ThSens OMap with
theoremStatus == Proof_status proof_tree
version_nr is updated for changed ThSens structure
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5250 cec4b9c1-7d33-0410-9eda-942365e851bb |
13ed13e06a5dd4aad12044ed7e7503cbe7f62990 |
|
19-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
merged in Tina's branch
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5216 cec4b9c1-7d33-0410-9eda-942365e851bb |
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0 |
|
29-Sep-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
expanded tabs to spaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5106 cec4b9c1-7d33-0410-9eda-942365e851bb |
82901c67e399ee530654da46ce7a849ec9b907eb |
|
13-Aug-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
made refute work with empty theories
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4910 cec4b9c1-7d33-0410-9eda-942365e851bb |
b565cd55a13dbccc4e66c344316da525c961e4ca |
|
16-Jul-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added coding of partiality and subsorting for CoCASL; properly renamed some encodings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4684 cec4b9c1-7d33-0410-9eda-942365e851bb |
42c01284bba8d7c8d995c8dfb96ace57d28ed1bc |
|
15-Jul-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactoring: [Pos] replaced with Range in order to exclude positions from equality of abstract syntax
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4671 cec4b9c1-7d33-0410-9eda-942365e851bb |
92303a4d15dffd2c571d32311dcae866bd449d86 |
|
06-Jul-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Isabelle.CreateThy and Isabelle.IsaProve use now the functions for
the desambiguation of sentence names implemented in Common.ProofUtils
instead of a local implementation.
CreateThy.createTheoryText disambiguates now all sentence names before
they are split for the pretty printing.
Naming and disambigutation functions are moved from Isabelle.IsaProve
to Common.ProofUtils.
Isabelle.Translate: charMap is moved to Common.ProofUtils so that each
prover has access to the same map for the translation of forbidden
characters.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4562 cec4b9c1-7d33-0410-9eda-942365e851bb |
f3a94a197960e548ecd6520bb768cb0d547457bb |
|
15-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
aligned module description for haddock-0.7
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4438 cec4b9c1-7d33-0410-9eda-942365e851bb |
97018cf5fa25b494adffd7e9b4e87320dae6bf47 |
|
15-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced Licence with License for haddock-07
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4433 cec4b9c1-7d33-0410-9eda-942365e851bb |
b4fbc96e05117839ca409f5f20f97b3ac872d1ed |
|
13-Jun-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added maintainers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4412 cec4b9c1-7d33-0410-9eda-942365e851bb |
8b5f9f72ba210940b26034bcadd34b2fe7f93bbd |
|
31-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
restructered Logic.Prover
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4345 cec4b9c1-7d33-0410-9eda-942365e851bb |
fa941cafef82113297227345cbb21e523f962cbe |
|
25-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
changed an import and a type synonim
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4331 cec4b9c1-7d33-0410-9eda-942365e851bb |
68f8cb9ffb303f207a7a7f985f6585726e545361 |
|
13-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed isSimpleRule
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4274 cec4b9c1-7d33-0410-9eda-942365e851bb |
3015a81bddf37523e8a2e9c4e29218d8d57b3c9b |
|
13-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
minor changes to match new IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4273 cec4b9c1-7d33-0410-9eda-942365e851bb |
9211d12224eaace6045457b313b97e4ab86f2479 |
|
03-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed Isabelle sentence type
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4190 cec4b9c1-7d33-0410-9eda-942365e851bb |
b960d107d9fcf19c77a460e082e5cc40b86621ec |
|
03-May-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
change in type Sentence
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4180 cec4b9c1-7d33-0410-9eda-942365e851bb |
e404133a2e2be28b886270f28b7134a0da6a7f6e |
|
28-Apr-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed translation of Isabelle strings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4154 cec4b9c1-7d33-0410-9eda-942365e851bb |
7f6b97541fdee30d62a0a3cfa58173212a6cd002 |
|
28-Apr-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
introduced an enumeration type for the Isabelle base signatures
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4151 cec4b9c1-7d33-0410-9eda-942365e851bb |
fb5587152ca9e32b1666be9094690b6420702039 |
|
16-Apr-2005 |
Tina Kraußer <tina@krausser.net> |
first simplifier-rules implemented
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4070 cec4b9c1-7d33-0410-9eda-942365e851bb |
a89b8e34869c9b735470c608638b112c14226644 |
|
02-Apr-2005 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added 'method_setup'
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4001 cec4b9c1-7d33-0410-9eda-942365e851bb |
7bd5754e08c0e163f96fff840189a38394f96af0 |
|
29-Mar-2005 |
Tina Kraußer <tina@krausser.net> |
showIsaT and showIsaIT are extented versions of showIsa and showIsaI which have an additional parameter for the Isabelle-theory
all occurrences of showIsa and showIsaI are substituted by the new functions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3994 cec4b9c1-7d33-0410-9eda-942365e851bb |
729aff22a7983f5bb113dcc604157edd728c1484 |
|
02-Mar-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
introduced default morphisms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3896 cec4b9c1-7d33-0410-9eda-942365e851bb |
fef23f00a053d23cdf32ba8f553b1147d7ff2d6e |
|
16-Feb-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
uncommented closeChildProcessFds
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3803 cec4b9c1-7d33-0410-9eda-942365e851bb |
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095d |
|
02-Feb-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
adapted to new IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3763 cec4b9c1-7d33-0410-9eda-942365e851bb |
d6025ee06343191f356a59704d467866afa29900 |
|
25-Jan-2005 |
Paolo Torrini <paolot@informatik.uni-bremen.de> |
modified according to new IsaSign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3708 cec4b9c1-7d33-0410-9eda-942365e851bb |
72c9a437f01021819bd23569d324bf47b989918d |
|
14-Jan-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved let to where block
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3675 cec4b9c1-7d33-0410-9eda-942365e851bb |
348fe871ff4d478f7bad37ea199edeeac3e17e04 |
|
14-Jan-2005 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Completed proved theory string.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3674 cec4b9c1-7d33-0410-9eda-942365e851bb |
2500f987b722d80582fff89b41323a200319110e |
|
13-Jan-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added final newline
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3666 cec4b9c1-7d33-0410-9eda-942365e851bb |
58307ff0b6f14c07dc09ced0b0bc53a36fdd4c99 |
|
10-Jan-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Changed HETS_ISABELLE: points now to binary
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3645 cec4b9c1-7d33-0410-9eda-942365e851bb |
3522f9599265731415f169549a47a70e8b02758a |
|
02-Dec-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
moved thyPath back to start of file (needed for imports)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3508 cec4b9c1-7d33-0410-9eda-942365e851bb |
5308ef83ee1b668f4cf6c8278bc645e7e0f8b4ed |
|
26-Nov-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Connected Isabelle consistency checker
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3468 cec4b9c1-7d33-0410-9eda-942365e851bb |
7ed2a775680fb1a29e6907d372124906b7746420 |
|
15-Nov-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Proof status interface reduced to names of axioms/thms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3429 cec4b9c1-7d33-0410-9eda-942365e851bb |
320f3c1dbac5a61f4e74827b5c5ec7e31f66e07e |
|
09-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
separate translations of labels and ids
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3407 cec4b9c1-7d33-0410-9eda-942365e851bb |
e79472ac9f45b44b205357ff33965c36bfe6f765 |
|
09-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
separated translation from printing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3406 cec4b9c1-7d33-0410-9eda-942365e851bb |
a348b2eb46eb51f376c910d6dd4415fdab6713bd |
|
08-Nov-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
IsaProve does not need cpp
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3395 cec4b9c1-7d33-0410-9eda-942365e851bb |
cbbb78891abe723a504c41d4722986589fdf336a |
|
25-Oct-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added /bin to HETS_ISABELLE
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3319 cec4b9c1-7d33-0410-9eda-942365e851bb |
3701dec6c273b6c7e46f89163fcd7f772db42ff4 |
|
21-Oct-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3308 cec4b9c1-7d33-0410-9eda-942365e851bb |
b172714c339053a40393dc0cf4f9151c97695e01 |
|
19-Oct-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added showLemmas flag to Isabelle signs, to chose whether lemmas with
simplified axioms should be included or not
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3270 cec4b9c1-7d33-0410-9eda-942365e851bb |
52a5c49b7e6d1dbff2e298d7287282fd84002489 |
|
14-Oct-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Replaced dummyT with noType
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3250 cec4b9c1-7d33-0410-9eda-942365e851bb |
840ad39a5a571d5170e7bc4796058208502fa73f |
|
08-Oct-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Added necessary term printing (because of changes in HasCASL2Isabelle)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3230 cec4b9c1-7d33-0410-9eda-942365e851bb |
87b7a494f805b2b2f3311564f3dfcc4352f803fc |
|
06-Sep-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
todo
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3134 cec4b9c1-7d33-0410-9eda-942365e851bb |
f4505a64a089693012a3f5c3b1f12a82cd7a2a5a |
|
30-Aug-2004 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Improved conditional compilation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3121 cec4b9c1-7d33-0410-9eda-942365e851bb |
6e049108aa87dc46bcff96fae50a4625df1d9648 |
|
30-Aug-2004 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Setup preprocessing for haddock; make doc works again
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3119 cec4b9c1-7d33-0410-9eda-942365e851bb |
31c49f2fa23d4ac089f35145d80a224deb6ea7e4 |
|
28-Aug-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added flag UNI_PACKAGE to allow removal of UniForM workbench
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3112 cec4b9c1-7d33-0410-9eda-942365e851bb |
aef2ec6fe7797a29aae26cbcbdb70e6ec0eb0f5b |
|
25-Aug-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Adapted printing.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3086 cec4b9c1-7d33-0410-9eda-942365e851bb |
1f084d62dbf8ae72357697c226cacd1973f0c03f |
|
10-Aug-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Keep old tactic scripts
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3046 cec4b9c1-7d33-0410-9eda-942365e851bb |
74fc328292d911eff0baa47a247005cf33d2bdd2 |
|
09-Aug-2004 |
Sonja Gröning <sonja@informatik.uni-bremen.de> |
Chossing the 'Prove'-option at node in a devGraph causes Isabelle to be opened with the translated specification
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3028 cec4b9c1-7d33-0410-9eda-942365e851bb |
3bfb47b9efda0a34324fa9cacd8d69ba0819a2c8 |
|
28-Jul-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
no need for dialog feedback and early dependency on uni stuff
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2989 cec4b9c1-7d33-0410-9eda-942365e851bb |
ce8b15da31cd181b7e90593cbbca98f47eda29d6 |
|
22-Jul-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Completed PCFOL2FOL
Modularized CoCASL2ISabelleHOL
(Partly) solved Qual_var problem in Overload
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2969 cec4b9c1-7d33-0410-9eda-942365e851bb |
6caada8926a23123aee618f61d64fe82cfd6e91e |
|
10-May-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added freeness flag to Sort_gen_ax; new transformation to Isabelle lexis
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2574 cec4b9c1-7d33-0410-9eda-942365e851bb |
2b4130336e941b7d01c78a6da55449a4c6eca609 |
|
23-Mar-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Refactoring for smooth integration of CASL extensions.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2310 cec4b9c1-7d33-0410-9eda-942365e851bb |
c529224e0ec191fbaa87261f05c34f89c17b3f3a |
|
15-Mar-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Debugging of proof support; problem with optimized unions fixed
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2277 cec4b9c1-7d33-0410-9eda-942365e851bb |
aa0ef8adb2833838c1954e6f93c61d85d2cb226a |
|
14-Mar-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Prover interface cont'd
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2275 cec4b9c1-7d33-0410-9eda-942365e851bb |