Permalink
Browse files

Delete some unnecessary infix declarations.

  • Loading branch information...
mn200 committed Oct 24, 2011
1 parent 0a0988f commit 1a6d3e93a2be38bc0bd8c73ae60e5a3901739f42
Showing with 0 additions and 4 deletions.
  1. +0 −4 src/temporal/src/Temporal_LogicScript.sml
@@ -6,10 +6,6 @@ open HolKernel Parse boolLib numLib pairLib
numTheory prim_recTheory arithmeticTheory pairTheory
Rsyntax schneiderUtils;
-infixr 3 -->;
-infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL;
-
-
val _ = new_theory "Temporal_Logic";
fun TAC_PROOF(g,t) = Tactical.TAC_PROOF(g,t) handle e => Raise e;

0 comments on commit 1a6d3e9

Please sign in to comment.