Context Navigation

- Modified Isabelle Proof Commands such that the + symbol can be used to repeat the command in Isabelle - Changed CspCASLProver to use the above Proof Commands - CspCASLProver now produces much more efficient code for the reflexivity, symmetry and transitivity proofs.

13:15 Changeset [11576] by csliam

trunk/Isabelle/IsaConsts.hs

Added "open" as an ignored key word in Isabelle

11:31 Changeset [11575] by maeder

trunk/OMDoc/HetsDefs.hs
trunk/OMDoc/OMDocInput.hs

OMDoc generation before changeset:11573 treated free def links implicitely. This is now restored, although OMDocInput never (re-)create(s/d) free def links.

24.03.2009:

18:10 Changeset [11574] by maeder

trunk/PGIP/InfoCommands.hs
trunk/Static/DevGraph.hs
trunk/Static/PrintDevGraph.hs

do not match on strings

17:32 Changeset [11573] by maeder

trunk/GUI/Glade/LinkTypeChoice.glade
trunk/GUI/GraphMenu.hs
trunk/Interfaces/Utils.hs
trunk/OMDoc/Export.hs
trunk/OMDoc/HetsDefs.hs
trunk/OMDoc/OMDocInput.hs
trunk/OMDoc/OMDocOutput.hs
trunk/OWL/StructureAnalysis.hs
trunk/PGIP/Utils.hs
trunk/Proofs/Composition.hs
trunk/Proofs/ComputeColimit.hs
trunk/Proofs/DGFlattening.hs
trunk/Proofs/EdgeUtils.hs
trunk/Proofs/Global.hs
trunk/Proofs/HideTheoremShift.hs
trunk/Proofs/Local.hs
trunk/Proofs/NormalForm.hs
trunk/Proofs/SimpleTheoremHideShift.hs
trunk/Proofs/TheoremHideShift.hs
trunk/Static/AnalysisArchitecture.hs
trunk/Static/AnalysisLibrary.hs
trunk/Static/AnalysisStructured.hs
trunk/Static/ArchDiagram.hs
trunk/Static/DevGraph.hs
trunk/Static/DotGraph.hs
trunk/Static/PrintDevGraph.hs

refactored link types

13:27 Changeset [11572] by maeder

trunk/DFOL/ATC_DFOL.der.hs
trunk/DFOL/ATC_DFOL.hs

removed generated files from svn

13:22 Changeset [11571] by maeder

trunk/GUI/GraphAbstraction.hs
trunk/GUI/ShowLibGraph.hs

made it compile with old uni

00:13 Ticket #674 (Endless error output) closed by raider

fixed: fixed in changeset:11570

00:12 Changeset [11570] by raider

trunk/GUI/GraphAbstraction.hs
trunk/GUI/GraphMenu.hs
trunk/GUI/ShowLibGraph.hs

Exiting UDrawGraph and all open windows, when all developement graph and library graph windows are closed. uses new function from uni, so a uni must be updated first. fixes ticked #674

23.03.2009:

23:02 Changeset [11569] by kristina

trunk/DFOL/Test_AS_DFOL.hs
trunk/DFOL/Test_Parse_AS_DFOL.hs
trunk/DFOL/Tests
trunk/DFOL/Tests/Matrices.het
trunk/DFOL/Tests/Test_AS_DFOL.hs
trunk/DFOL/Tests/Test_Parse_AS_DFOL.hs

22:43 Ticket #679 (Translate Graph goes wrong) closed by raider

fixed: fixed in changeset:11568

22:40 Changeset [11568] by raider

trunk/GUI/GraphLogic.hs
trunk/GUI/GraphMenu.hs
trunk/GUI/ShowLibGraph.hs

moved graph translation menu to library graph menu.

22:13 Changeset [11567] by kristina

trunk/DFOL/ATC_DFOL.der.hs
trunk/DFOL/ATC_DFOL.hs

22:08 Changeset [11566] by kristina

trunk/DFOL/Logic_DFOL.hs
trunk/DFOL/Morphism.hs
trunk/DFOL/Sign.hs
trunk/Makefile

Implemented Logic_DFOL to integrate the DFOL parser into Hets

13:26 Changeset [11565] by maeder

trunk/doc/UserGuide.tex

corrected Factorial (and Buffer) example (removed trailing white space)

11:09 Changeset [11564] by maeder

trunk/CspCASL/Logic_CspCASL.hs

replaced german text

10:57 Changeset [11563] by maeder

trunk/Driver/Version.in

removed umlaut

10:53 Changeset [11562] by maeder

trunk/Makefile

removed umlaut

10:50 Changeset [11561] by maeder

trunk/Makefile

added DFOL to SOURCE_PATHS

10:09 Changeset [11560] by maeder

trunk/Makefile

added logic DFOL

01:02 Changeset [11559] by kristina

trunk/DFOL/AS_DFOL.hs
trunk/DFOL/Logic_DFOL.hs
trunk/DFOL/Parse_AS_DFOL.hs
trunk/DFOL/Test_Parse_AS_DFOL.hs

Added first implementation of Logic class for DFOL to integrate the DFOL parser into HETS

22.03.2009:

16:35 Ticket #678 (Distinguish local and global theorem links in the command line interface) closed by rpascanu

fixed

16:35 Ticket #466 (sync command line interface (PGIP) with GUI) closed by rpascanu

fixed

16:35 Ticket #655 (proof-commands not recognized in proof-script history) closed by rpascanu

fixed

16:34 Changeset [11558] by rpascanu

trunk/GUI/GraphMenu.hs
trunk/GUI/Utils.hs
trunk/PGIP/Commands.hs
trunk/PGIP/ConsCommands.hs
trunk/PGIP/Shell.hs
trunk/PGIP/Utils.hs

Fixed ticket 678, 466, 655

20.03.2009:

18:55 Changeset [11557] by ewaryst

trunk/OMDoc/XmlInterface.hs

removed testpart and added omobj output in requations

18:17 Ticket #43 (assign a unique origin to Hets symbols in OMDoc) closed by ewaryst

fixed: can be done with the non-disjoint-unions flattening

18:15 Ticket #44 (output OMDoc as shared XML structure) closed by ewaryst

wontfix: As the ticket #2 won't be completed, this ticket can't be completed …

18:12 Ticket #488 (look at Hets and OMDoc datastructures) closed by ewaryst

fixed: I had a look on that…

18:08 Ticket #495 (check if projection is needed for Cast) closed by ewaryst

fixed: Obsolete code

18:05 Ticket #529 (simplify constant types) closed by ewaryst

fixed: The new export doesn't contain this error

18:02 Ticket #39 (discuss OmDoc output with Immanuel) closed by ewaryst

fixed: Discussing already with Florian

15:29 Changeset [11556] by maeder

trunk/OMDoc/Export.hs

change node name

15:10 Changeset [11555] by ewaryst

trunk/OMDoc/XmlInterface.hs

renamed view in theory-inclusion

14:30 Changeset [11554] by ewaryst

trunk/OMDoc/DataTypes.hs
trunk/OMDoc/Export.hs
trunk/OMDoc/XmlInterface.hs

added export of the morphisms

14:30 Changeset [11553] by ewaryst

trunk/CASL/OMDoc.hs

added export of the morphisms

14:29 Changeset [11552] by ewaryst

trunk/Logic/Logic.hs

removed the libid and specid from the omdoc-morphism export

19.03.2009:

20:49 Changeset [11551] by maeder

trunk/Proofs/QualifyNames.hs

fixed #677

20:01 Changeset [11550] by maeder

trunk/Proofs/VSE.hs

qualify the whole libEnv

18:44 Changeset [11549] by till

trunk/doc/UserGuide.tex

eliminated hets@...

12:15 Ticket #673 (Possibility of multiple open windows broken) closed by maeder

fixed: fixed by changeset:11503

11:59 Ticket #679 (Translate Graph goes wrong) created by maeder

Currently hets fails after "Edit -> Translate Graph" with:[…]

18.03.2009:

21:41 Changeset [11548] by kristina

trunk/DFOL/AS_DFOL.hs
trunk/DFOL/Parse_AS_DFOL.hs
trunk/DFOL/Test_AS_DFOL.hs
trunk/DFOL/Test_Parse_AS_DFOL.hs
trunk/DFOL/Utils.hs

17:53 Changeset [11547] by maeder

trunk/CASL/ToSExpr.hs
trunk/Proofs/VSE.hs

create theorem VSE links

16:37 Changeset [11546] by maeder

trunk/CASL/Qualify.hs

make sort, op and pred names distinct for VSE

16:23 Changeset [11545] by maeder

trunk/CASL/Qualify.hs

simplified

16:02 Changeset [11544] by maeder

trunk/Driver/WriteFn.hs
trunk/GUI/GraphLogic.hs
trunk/Interfaces/Utils.hs
trunk/PGIP/DataTypesUtils.hs
trunk/PGIP/DgCommands.hs
trunk/Proofs/DGFlattening.hs
trunk/Proofs/InferBasic.hs
trunk/Proofs/Local.hs
trunk/Proofs/TheoremHideShift.hs

refactored or reverted computeTheory

11:40 Changeset [11543] by maeder

trunk/Propositional/Logic_Propositional.hs

implemented isInclusion method (and cleaned up)

11:12 Changeset [11542] by maeder

trunk/Driver/AnaLib.hs

allow to switch on normal form computation via command line arguments

10:54 Changeset [11541] by maeder

trunk/Proofs/Automatic.hs

remove normal form computation from automatic

10:51 Changeset [11540] by maeder

trunk/Driver/Options.hs

added flag for normal form computation

10:23 Changeset [11539] by maeder

trunk/Comorphisms/CASL2Prop.hs

made translation monadic rather than throwing an error

17.03.2009:

21:48 Changeset [11538] by kristina

trunk/DFOL/Test_AS_DFOL.hs
trunk/DFOL/Test_Parse_AS_DFOL.hs

Adding tests for DFOL abstract syntax and parser

17:56 Changeset [11537] by maeder

trunk/INSTALL

adjusted installation text

16:51 Changeset [11536] by maeder

trunk/Comorphisms/CASL2Prop.hs
trunk/Comorphisms/LogicGraph.hs

added CASL2Prop

16:16 Changeset [11535] by maeder

trunk/Comorphisms/CASL2Prop.hs

an inverse comorphism of Prop2CASL

14:21 Changeset [11534] by maeder

trunk/Propositional/Analysis.hs
trunk/Propositional/Logic_Propositional.hs
trunk/Propositional/Morphism.hs
trunk/Propositional/Parse_AS_Basic.hs
trunk/Propositional/Sign.hs
trunk/Propositional/Symbol.hs

implemented missing stuff

12:38 Changeset [11533] by kristina

trunk/DFOL/AS_DFOL.hs

Pretty printing modified to match specification syntax

16.03.2009:

23:25 Changeset [11532] by kristina

trunk/DFOL/AS_DFOL.hs
trunk/DFOL/Parse_AS_DFOL.hs

Parsing tested

17:53 Changeset [11531] by kristina

trunk/DFOL/AS_DFOL.hs
trunk/DFOL/Logic_DFOL.hs
trunk/DFOL/Parse_AS_DFOL.hs
trunk/DFOL/test.hs

Adding parser for DFOL abstract syntax

16:17 Ticket #678 (Distinguish local and global theorem links in the command line interface) created by till

Currently, with the attached file, I get[…]

15:50 Ticket #574 (Avoid code duplication in PGIP.ConsCommands) closed by rpascanu

fixed

15:31 Changeset [11530] by maeder

trunk/Comorphisms/CASL2HasCASL.hs

nullary predicates goto ?Unit

14:42 Changeset [11529] by luecke

trunk/OWL/tests/beer.owl
trunk/OWL/tests/pizza.owl
trunk/OWL/tests/wine.rdf

new test cases

11:42 Changeset [11528] by maeder

trunk/DFOL/test.hs

avoid clash for Test.hs on Macs with a case-insensitiv file system

15.03.2009:

22:56 Changeset [11527] by rpascanu

trunk/Interfaces/History.hs
trunk/Interfaces/Utils.hs

duplicate code ticket solved

22:55 Changeset [11526] by rpascanu

trunk/GUI/GraphLogic.hs
trunk/GUI/Utils.hs

duplicate code ticket solved

22:55 Changeset [11525] by rpascanu

trunk/PGIP/Commands.hs
trunk/PGIP/ConsCommands.hs
trunk/PGIP/UndoRedo.hs

duplicate code ticket solved

18:03 Changeset [11524] by csliam

trunk/CspCASL/AS_CspCASL_Process.der.hs
trunk/CspCASL/Print_CspCASL.hs
trunk/CspCASL/SignCSP.hs
trunk/CspCASL/SimplifySen.hs
trunk/CspCASLProver.hs
trunk/CspCASLProver/CspCASLProver.hs
trunk/CspCASLProver/CspProverConsts.hs
trunk/CspCASLProver/TransProcesses.hs
trunk/Isabelle/IsaConsts.hs

Improved pretty printing of typed channels in CspCASL

00:58 Changeset [11523] by kristina

trunk/Common/Keywords.hs

14.03.2009:

23:28 Changeset [11522] by kristina

trunk/test.hs

Test file for AS_DFOL

23:27 Changeset [11521] by kristina

trunk/Common/Keywords.hs
trunk/DFOL/AS_DFOL.hs
trunk/DFOL/Logic_DFOL.hs

Modified abstract syntax for DFOL to permit declarations of type k,l:Int instead of k:Int, l:Int.

13.03.2009:

22:12 Changeset [11520] by maeder

trunk/utils/DrIFT-src/ChaseImports.hs

windows changes colons to semicolons

21:18 Changeset [11519] by maeder

trunk/Comorphisms/PPolyTyConsHOL2IsaUtils.hs

do not split off definedness on leaves

21:06 Changeset [11518] by maeder

trunk/Comorphisms/PCoClTyConsHOL2IsabelleHOL.hs
trunk/Comorphisms/PCoClTyConsHOL2PairsInIsaHOL.hs
trunk/Comorphisms/PPolyTyConsHOL2IsaUtils.hs

propagate simplifier options

20:29 Changeset [11517] by ewaryst

trunk/OMDoc/DataTypes.hs
trunk/OMDoc/Export.hs
trunk/OMDoc/XmlInterface.hs

views and imports commenced

20:07 Changeset [11516] by maeder

trunk/Comorphisms/PPolyTyConsHOL2IsaUtils.hs

corrected Unit2bool conversion

16:18 Changeset [11515] by ewaryst

trunk/Driver/WriteFn.hs

omdoc devgraph export hooked in under exp

16:17 Changeset [11514] by ewaryst

trunk/CASL/OMDoc.hs

filtering out nonlocal signature elems

16:17 Changeset [11513] by ewaryst

trunk/OMDoc/Export.hs
trunk/OMDoc/XmlInterface.hs

added the overall export of the devgraph

14:16 Changeset [11512] by ewaryst

trunk/CASL/OMDoc.hs

filtering out the non local signature elements

14:15 Changeset [11511] by ewaryst

trunk/OMDoc/XmlInterface.hs

only changed the testpart

12:07 Ticket #677 (ShowTheory fails after Qualify Names in Union Specification) created by ewaryst

The following spec produce this error (same names from the two imported …

12.03.2009:

16:57 Changeset [11510] by maeder

trunk/Comorphisms/PPolyTyConsHOL2IsaUtils.hs

correct lambda term in Hets-lib/HasCASL/Functions.het

15:06 Changeset [11509] by maeder

trunk/Comorphisms/PPolyTyConsHOL2IsaUtils.hs

fixed Calculi/Time/AllenHayesLadkin_TACAS example

09:22 Changeset [11508] by maeder

trunk/DFOL/AS_DFOL.hs

added missing import of Common.AS_Annotation removed trailing white space and untabified

11.03.2009:

23:15 Changeset [11507] by kristina

trunk/DFOL/AS_BASIC_DFOL.hs
trunk/DFOL/AS_DFOL.hs
trunk/DFOL/Logic_DFOL.hs

Modified DFOL abstract syntax to allow axioms interspersed with signature declarations

Note: See TracTimeline for information about the timeline view.

Download in other formats:

RSS Feed